On 2/12/13 5:47 PM, Nehal Patel wrote:
And so my question is, that in 2013, why isn't this process a full fledged part of the language? I imagine I just don't know what I'm talking about, so correct me if I'm wrong, but this is how I understand the workflow used in practice with program derivation: 1) state the problem pedantically in code, 2) work out a bunch of proofs with pen and paper, 3) and then translate that back into code, perhaps leaving you with function_v1, function_v2, function_v3, etc -- that seems fine for 1998, but why is it still being done this way?
I think there's a lot more complexity in (machine-verifiably) proving things than you realize. I've done a fair amount of programming in Coq and a bit in Twelf and Agda, and one of the things I've learned is that the kinds of proof we do on paper are rarely rigorous and are almost never spelled out in full detail. That is, afterall, not the point of a pen & paper proof. Pen & paper proofs are about convincing humans that some idea makes sense, and humans are both reasonable and gullible. Machine-verified proofs, on the other hand, are all about walking a naive computer through every possible contingency and explaining how and why things must be the case even in the worst possible world. There's no way to tell the compiler "you know what I mean", or "the other cases are similar", or "left as an exercise for the reader". And it's not until trying to machine-formalize things that we realize how often we say things like that on paper. Computers are very bad at generalizing patterns and filling in the blanks; but they're very good at exhaustively enumerating contingencies. So convincing a computer is quite the opposite from convincing a human.
That said, I'm all for getting more theorem proving goodness into Haskell. I often lament the fact that there's no way to require proof that instances obey the laws of a type class, and that GHC's rewrite rules don't require any proof that the rule is semantics preserving. The big question is, with things as they are today, does it make more sense to take GHC in the direction of fully-fledged dependent types? or does it make more sense to work on integration with dedicated tools for proving things?
There's already some work towards integration. Things like Yices and SBV can be used to prove many things, though usually not so much about programs per se. Whereas Liquid Haskell[1] is working specifically toward automated proving of preconditions and postconditions.
[1] <http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/> -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
