The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I'm writing to announce another "release" of my work-in-progress online book on program proof in Coq:
    http://adam.chlipala.net/frap/
It's called Formal Reasoning About Programs.  I've used it in two graduate classes so far, and I made another announcement about a year ago about an earlier version.  The current version is further tested and improved, including with new early tutorial material on Coq and with new chapters on data abstraction and compiler verification.

Some subscribers of this mailing list might want to consider running FRAP classes at their own institutions.  I think the book and associated materials are now well-enough developed to make that not a crazy idea, and I'm happy to provide personalized support in adapting the class to different settings.  Please do let me know if you're considering such an experiment.

In terms of educational goals, FRAP is a cousin to Software Foundations.  FRAP also aims to introduce Coq to a general computer-science audience, and it also aims to introduce classic semantics and program-proof techniques using Coq.  A crucial difference, though, is that FRAP assumes familiarity with topics like proof by induction -- which we generally "teach" to all CS undergraduates but, unfortunately, expect few to master.  Students need to be comfortable with both rigorous proofs and programming to keep up with FRAP, though they shouldn't need to come in with any experience in formal methods or functional programming.

The payoff from the higher starting expectations is getting through more of the PL canon.  I can testify that multiple students with no prior formal-methods experience have accomplished the following by the end of the class, taking a sampling of our assignments.  (Admittedly, more such students drop the class than hang on to the end, but I'm still working on tweaking the "gentle on-ramp" aspect!)

• Write mostly automated correctness proofs that a classic lock algorithm achieves mutual exclusion.
• Verify a producer-consumer program by choosing a proper abstraction and then automatically model-checking the resulting system inside Coq.
  
• Prove soundness of a logical relation and use it to demonstrate contextual equivalence of two implementations of a simple abstract data type.
• Verify particular C-like programs using separation logic, with the level of proof automation we expect from standalone verification tools.
• Prove that, in a shared-memory concurrent language, a global lock order avoids deadlock.
• Prove soundness of rely-guarantee for shared-memory concurrent programs, and use it to verify example programs.

A nontrivial Coq library is behind the class, including both an alternative suite of basic tactics, to avoid some common beginner hang-ups; and a set of parameterized proof-automation engines, principally for model checking, abstract interpretation, and discharging verification conditions from separation logic.  Almost all the proof techniques in the class are cast in terms of the common formalism of state transition systems and their invariants, a commonality that I find isn't emphasized often enough in semantics classes.  (For instance, when we get to type soundness and the "progress and preservation" conditions behind the widely used syntactic approach, we see that they are just a special case of the principles of invariant induction and invariant strengthening that we have been using all along!)

I'll be very glad to hear from anyone interested in test-driving the material.