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

[Chaddaï Fouché]

2008/9/14 Rafael Almeida <almeidaraf at gmail.com>:
>
> 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?

Well, that's where formal prover enter the picture : when you prove
something with Coq, you can be reasonably sure that your proof is
correct. And FM brings absolute certitude a propriety is verified by
your program whereas testing however heavy can only check this
property on a finite set of inputs (using randomly generated input
help alleviate the risk of blind spot but is still limited).

-- 
Jedaï