Should exhaustiveness testing be on by default?
ndmitchell at gmail.com
Thu May 21 11:49:32 EDT 2009
>> 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
> * 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.
More information about the Glasgow-haskell-users