<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I wrote to this list about five years ago to announce <a moz-do-not-send="true" href="https://urldefense.com/v3/__http://adam.chlipala.net/frap/__;!!IBzWLUs!Ho35lUfjPJUkwg5ptsUd2q0dFW8DrngklYI7vMhA2DAe2G1GU26RzJHRnLlaYYmaJJphvfdzudFdXQ$"><i>Formal
Reasoning About Programs</i></a> (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.</p>
<p>What's different about FRAP as compared to e.g. <i>Software
Foundations</i>, the alternative I know best?</p>
<p><u><b>Cons</b></u></p>
<ul>
<li>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 <i>Software Foundations</i>
does a good job of reinforcing those topics for students who
never really "got" them the first time around (doing proofs
without machine checking).</li>
</ul>
<p><u><b>Pros</b></u></p>
<ul>
<li>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.</li>
<li>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.</li>
<li>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 moz-do-not-send="true" href="https://urldefense.com/v3/__http://adam.chlipala.net/papers/FrapICFP21/__;!!IBzWLUs!Ho35lUfjPJUkwg5ptsUd2q0dFW8DrngklYI7vMhA2DAe2G1GU26RzJHRnLlaYYmaJJphvfeVU-tIow$">a
functional-pearl paper on this part at ICFP in about two weeks</a>,
and I'll be available in the associated Q&A sessions.</li>
</ul>
<p>I'm glad to discuss by whatever medium with folks who might want
to make use of these materials.<br>
</p>
</body>
</html>