On Sun, Sep 14, 2008 at 5:56 AM, Thomas M. DuBuisson
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?