[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

[Thomas M. DuBuisson]

> What would theorem proofs do for me?   
Imagine if you used SmallCheck to exhastively test the ENTIRE problem
space for a given property.  Now imagine you used your brain to show the
programs correctness before the heat death of the universe...

Proofs are not features, nor are they code.  What you prove is entirely
up to you and might not be what you think.  Take, for example, the issue
of proving a sort function works correctly [1].

I'm not saying this to discourage complete proofs, but just cautioning
you that proving something as unimportant and IO laden as an IRC bot
probably isn't the best example.  Do see the linked PDF, and [2] as
well.

Oh, and for examples where people should have used FM, search for
'ariane 1996'  or the gulf war patriot missle failure

TomMD

[1]
http://www.cl.cam.ac.uk/~mjcg/Teaching/SpecVer1/Lectures/pslides07x4.pdf
[2] http://users.lava.net/~newsham/formal/reverse/