[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008
almeidaraf at gmail.com
Sun Sep 14 06:59:06 EDT 2008
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 .
> 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  as
> Oh, and for examples where people should have used FM, search for
> 'ariane 1996' or the gulf war patriot missle failure
>  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?
More information about the Haskell-Cafe