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_POPLmark_Challenge
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
