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/