[TYPES/announce] A book on program proof in Coq [revisited]

[Adam Chlipala]

I wrote to this list about five years ago to announce /Formal Reasoning 
About Programs/ <https://urldefense.com/v3/__http://adam.chlipala.net/frap/__;!!IBzWLUs!Ho35lUfjPJUkwg5ptsUd2q0dFW8DrngklYI7vMhA2DAe2G1GU26RzJHRnLlaYYmaJJphvfdzudFdXQ$ > (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 <https://urldefense.com/v3/__http://adam.chlipala.net/papers/FrapICFP21/__;!!IBzWLUs!Ho35lUfjPJUkwg5ptsUd2q0dFW8DrngklYI7vMhA2DAe2G1GU26RzJHRnLlaYYmaJJphvfeVU-tIow$ >, 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210811/892eec36/attachment.htm>