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

[Rafael Almeida]

On Sun, Sep 14, 2008 at 5:56 AM, Thomas M. DuBuisson
<thomas.dubuisson at gmail.com> wrote:
>
>> 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/
>

One thing have always bugged me: how do you prove that you have
correctly proven something? I mean, when I write a code I'm formaly
stating what I want to happen and bugs happen. If I try to prove some
part of the code I write more formal text (which generally isn't even
checked by a compiler); how can I be sure that my proof doesn't
contain bugs? Why would it make my program less error-prone? Is there
any article that tries to compare heavy testing with FM?