[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.
