2008/9/14 Rafael Almeida <[EMAIL PROTECTED]>: > > 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ï _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
