I feel we should really be able to use effects (and a little compile-time code analysisis) to break methods down into Always throws, vs May throw, vs Never throws
Probably even to getting a list of all exception types it might throw – should be a reasonable use of abstract interpetetation.
Just having “Always throws” or not is enough to eliminate a ton of the false positives – namely the ones that that come from stub definitions that just throw “NotImplementedException”. And that should just need effects.
I just haven’t got round to looking into it.