Should exhaustiveness testing be on by default?

[Neil Mitchell]

>> Catch already does assertion checking (1). Its runtime on moderate to
>> small programs (HsColour in particular) is far less than the time GHC
>> takes to compile them, and I still have no idea what its runtime is on
>> enormous programs (2). An analysis can be whole program and can be
>> slow, one does not imply the other.
>
> But the primary problem with Catch is that its analysis not well
> defined. I have no guarantee regarding the existence or not of false
> positives or false negatives, as Catch has no underlying formal logic to
> guide such reasoning.

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.

I guarantee that there are safe programs Catch can't prove safe, for a
proof see Turing 1937 :-)

Thanks

Neil