[Haskell-cafe] Why isn't "Program Derivation" a first class citizen?

[wren ng thornton]

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