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