Re: Coq proof assistant

[Michael Greenberg <michael.m.greenberg@gmail.com>]

Hi Paul,

Coq is a great tool!  Penn (where I am a PhD student) is a big Coq
school. ;)  We're the home of the POPLmark challenge
(http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/) which
exercises Coq (among other provers).  Benjamin Pierce, Chris
Casinghino and I wrote Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/), the course book for CIS 500,
the graduate level introduction to programming languages.  It uses Coq
to teach functional programming, simple imperative programs, the
simply-typed lambda calculus, and a few extensions to the lambda
calculus.  Naturally, I think it's a pretty good introduction to Coq.
:)  Some other Penn people---in particular, Aaron Bohannon and Brian
Aydemir---put on a (great!) tutorial at POPL08 in San Francisco
(http://www.cis.upenn.edu/~plclub/popl08-tutorial/).  It's targeted at
a rather technical audience, but it offers more realistic developments
than our book.  I hope some of those resources are useful for you.

I agree that Coq can be frustrating.  Some of us joke that Coq is the
assembly language of theorem proving---for example, it doesn't
directly support dependent pattern matching, so tactics have to
manually construct equalities.  At a higher level, I'm sometimes
frustrated by the rigidity of the tactic language.  (Though I haven't
tried using Ltac, which I hear is quite helpful.)  If you're looking
for alternatives, Agda is a general-purpose Haskell-inspired theorem
prover based on dependent pattern matching that some other people in
the department like.

Cheers,
Michael