Should exhaustiveness testing be on by default?

[Neil Mitchell]

>> If Catch says your program will not crash, then it will not crash. I
>> even gave an argument for correctness in the final appendix of my
>> thesis http://community.haskell.org/~ndm/thesis/ (pages 175-207). Of
>> course, there are engineering concerns (perhaps your Haskell compiler
>> will mis-translate the program to Core, perhaps the libraries will be
>> wrong, perhaps a bit in RAM will flip due to electrical interference),
>> but Catch has a formal basis.
>
> Oh, very good! I wasn't aware you'd tried this. I imagine you do
> something like:
>
>    * identify all partial functions
>    * bubble that information outwards, crossing off partial functions
>      that are actually total due to tests in callers that effectively
>      reduce the possible inhabitants of the types passed to the partial
>      function
>    * and you have some argument for why your travesal doesn't miss, or
>      mislabel constraints.

Nope, not at all. I assume all missing case branches are replaced with
calls to error (as both GHC and Yhc Core do), then prove that:

satE $ pre e ==> not $ isBottom $ eval e

If the preconditions generated by Catch on an expression are a
tautology, that implies the evaluation of e won't contain any _|_
terms at any level. If the precondition Catch generates is const True,
then that implies the evaluation is never bottom. I then proceed by
induction with a few lemmas, and fusing things - the "proof" is all at
the level of Haskell equational reasoning.

> Is it possible for Catch to print out its reasoning for why some
> function 'f' is total, such that I could check it (with another tool)?

It already does. My plan was always to output the reasoning into an
ESC/Haskell file, and then have the "Catch" process run the Catch
algorithm, and then check the results with ESC/Haskell - this way I
hoped to avoid writing a proof for Catch...

Things didn't quite turn out that way, as I needed to submit my
thesis, I didn't have a copy of ESC/Haskell good enough to do what I
wanted, and every thesis needs a nice proof in the appendix.

Thanks, Neil