On Sep 15, 2008, at 10:43 AM, Robin Green wrote:
In fairness, that's how it's often done in universities (where correctness doesn't really matter to most people - no offense intended). But once you start using software to write formal proofs, it is quite easy in principle to get a computer to check your proof for you. Many academics do not use formal proof tools because (a) they are not aware of them, or (b) they see them as too hard to learn, or (c) they see them as too time-consuming to use, or (d) they don't see the point. Hopefully this situation will gradually change.
Fortunately, I think it has been changing rather rapidly lately. In the last year or so, tools like Coq and Isabelle have become increasingly popular. Several universities now have classes: http://www.cs.colorado.edu/~siek/7000/spring07/ http://web.cecs.pdx.edu/~apt/cs510coq/ad http://www.cs.cmu.edu/~emc/15-820A/ http://www.cs.harvard.edu/~adamc/cpdt/ http://adam.chlipala.net/itp/ http://cl.cse.wustl.edu/classes/cse545/ There's a competition to solve various programming-languge-related problems using automated proof checkers: http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_... A tutorial at the last POPL conference: http://www.cis.upenn.edu/~plclub/popl08-tutorial/ And a number of projects with mechanical proofs: http://www.chargueraud.org/arthur/research/index.php http://compcert.inria.fr/doc/index.html http://ece-www.colorado.edu/~siek/segt_typesafe.pdf http://ece-www.colorado.edu/~siek/pubs/pubs/2005/siek05:_cpp_isar.pdf http://ece-www.colorado.edu/~siek/gradual-obj.pdf http://adam.chlipala.net/papers/ http://pauillac.inria.fr/~xleroy/proofs.html http://www.kennknowles.com/research/knowles-flanagan.draft.07.explicit.pdf I'm sure I've left out many of the most relevant examples, but this is a bit of the flavor of the recent work in the area. Aaron