The Coq mailing list

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

I wrote to this list about five years ago to announce Formal Reasoning About Programs (FRAP), an online book I've been developing to teach students some of the most classic approaches in program verification, using the Coq proof assistant.  In the mean time, I've used the book in four more editions of the class I teach with it, and I'm glad to report that the materials (including homework assignments) now seem to be in good shape for others to pick up and use at their institutions.  I'd be glad to correspond with anyone who's curious about perhaps offering a related course.

What's different about FRAP as compared to e.g. Software Foundations, the alternative I know best?

Cons

• From students, FRAP requires the levels of mathematical & programming sophistication that we associate with undergraduates just about finished with their CS degrees and headed to PhDs.  Students really do already need to be familiar with mathematical rigor and proof by induction, whereas Software Foundations does a good job of reinforcing those topics for students who never really "got" them the first time around (doing proofs without machine checking).

Pros

• As a result, we can get a lot further in sophistication of program-reasoning techniques.  For instance, I usually spend the last month or so of class on concurrency.  We look at shared-memory concurrency via model checking (with partial-order reduction) and concurrent separation logic (with shared mutable, linked data structures), and we look at message-passing concurrency via process calculus and session types.  Proofs are highly automated throughout, at the same time as all reasoning techniques are proved from first principles.
• I try to highlight commonalities across techniques that are rarely called out elsewhere.  For instance, about 3/4 of the techniques we look at (after the first month or so of class) are instances of finding and proving strengthened invariants for transition systems.  Then the rest are instances of finding simulation relations for pairs of labeled transition systems, and there is a clear family resemblance here to invariant-finding.  Common approaches to abstraction and modularity then apply throughout.
• We work up more quickly to more realistic programming languages, using a trick I call "mixed embeddings" that is somewhat similar to how Haskell imports side effects via monads.  We can add arbitrary side effects to Coq's core functional language, which lets us write and verify pretty sophisticated programs without needing to formalize the purely functional constructs we rely on.  At the same time, we can do most of the usual metatheory without compromising on rigor.  I have a functional-pearl paper on this part at ICFP in about two weeks, and I'll be available in the associated Q&A sessions.

I'm glad to discuss by whatever medium with folks who might want to make use of these materials.