[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

[Aaron Tomb]

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