2008/9/14 Rafael Almeida
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ï