[Pl-seminar] My spring class on Coq proofs of program correctness

[Adam Chlipala]

Some of you might be interested in participating in my spring class at 
MIT, so here's a bit of information on it:

MIT 6.887: Formal Reasoning About Programs

This class introduces two interrelated topics in parallel.
(1) Machine-checked mathematical proofs.  That is, we will use the Coq 
software package to check rigorous logical arguments automatically.
(2) Techniques for proving correctness of programs.  We will study how 
to formalize program behavior rigorously and how to prove that programs 
behave as expected.

In the second category, we will cover operational semantics, model 
checking, type systems, and program logics as the baseline techniques. 
In the last month or so of the course, we will also focus in on how to 
generalize these ideas to apply to concurrent programs (both 
shared-memory and message-passing).  Throughout, we will take note of 
how all the techniques we learn fit the common pattern of finding an 
invariant for a transition system, often applying abstraction and 
modularity techniques to decompose such problems into simpler ones.

Here is the course web site, which is still the one from last year but 
which will be updated over winter break.  It should still be helpful as 
a source of additional information.
   https://frap.csail.mit.edu/
The times and places of scheduled class meetings will be the same this 
spring.

Planned changes for the coming offering as compared to the last one:
(1) At least one of the two scheduled lectures each week will be spent 
on techniques for applying Coq effectively, primarily for automation of 
proofs.  Near the end of the course, we'll spend that time on case 
studies of mechanized reasoning "in practice" in significant research 
projects.  Likely examples include the instructor's ongoing projects in 
correctness of computer processors, file systems, compilers, concurrent 
data structures, database queries, parsers, or cryptographic primitives.
(2) Last term, all assignments were graded automatically, based on 
prompts to prove particular theorems.  This time, by popular demand, 
about once a month we'll have an assignment where students need to 
design their own formal systems (e.g., a set of proof rules for 
verifying a particular class of programs), not just prove correct ones 
provided by the course staff.
(3) Learning to use a proof assistant is hard, with all the little 
tricks of the trade that help save programmer time.  For getting started 
learning, best practices are to have "the expert down the hall" to ask 
questions to.  We'll try to simulate that mode by holding copious office 
hours, at least 10 hours per week; and we'll encourage students to hang 
out in office hours and help each other, too.