Lecture
Course material will be presented and discussed on this Zoom link during lectures on Tuesdays on Thursdays each week. Each lecture will be offered twice: once at 10am PT and again at 6:30pm PT. You can attend whichever lecture is most convenient for you, but should try to be in lecture at least once on Tuesdays and at least once on Thursdays. Each lecture will open with brief updates on the course.
Week 01 - Functional Programming and Proofs: Numbers, Lists, Trees
March 30- April 01 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
At the core of the Coq proof assistant lies a pure functional programming language with little more than functions and inductive data types (trees). Functional programming differs from object-oriented or imperative programming by de-emphasizing mutation, prioritizing expressions rather than statements, using recursion to express repetition, and treating functions as first-class values. Because "in math, there are no side effects," the Coq proof assistant takes these ideas even further by eliminating I/O, mutation, exceptions, etc., and by requiring all functions to terminate! While these limitations are severe, they enable completely formal proofs about programs, allowing us to prove our software correct. The primary mechanism for reasoning about trees and recursive functions is induction, which will be our best friend for the rest of the quarter.
Week 02 - Arith: Abstract Syntax; Semantics via Interpreters
April 06 - April 08 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
With the basics of Coq under our belt, we use the proof assistant as a laboratory to begin our study of programming languages. In some sense, programs are just data, namely, the string consisting of their source code. This string is called the "concrete syntax". We also study "abstract syntax," which is a tree derived from the string by parsing it. These notions of syntax have no inherent meaning, but are merely a way to write programs down. To give them meaning, we use semantics. The first kind of semantics we will study uses interpreters, which are recursive functions on the abstract syntax tree that execute a program to compute its final answer. We use these techniques to formalize and study a very simple language of arithmetic, with numerical constants, variables, addition, and multiplication. We also extend the language to include imperative features of assignment, if statements, and a restricted form of loops.
Week 03 - Transition Systems: Inductive Invariants
April 13, April 15 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
Last week we studied how to formalize programming languages in terms of their syntax (just inductive trees!) and interpreters (just recursive functions!). However, because all functions in Coq must be structurally recursive (i.e., terminating), we were not able to model the semantics of languages that have features like unbounded while loops.
This week we'll introduce the crucial mechanism needed to model the semantics of arbitrary programming languages: formalizing them as transition systems. Transition systems are really just (potentially infinite) state machines -- we describe them in terms of their sets of possible states, which states the system can start in, and when one state can transition to another state. The behavior of a program (when modeled as a transition system) can then be reasoned about in terms of the sets of states its execution can ever reach. Since that set of reachable states may be infinite, we'll need techniques for reasoning about it inductively.
Trying to prove invariants (properties that are true for all reachable states of a transition system) by induction can get stuck in a couple of ways:
We might find a "counterexample to safety" (CTS) where we discover a reachable state that does not satisfy our property.
In this case the property is not an invariant at all! Perhaps our program has a bug, or perhaps we misstated the property.
We might find a "counterexample to induction" (CTI) where we discover a state S1 such that our target property holds, but S1 can step to a state S2 where the property does not hold.
Even if we find a CTI, our target property may still be an invariant!
When we get stuck trying to verify example transition systems, we'll study how we can find stronger properties (true of fewer states) that are inductive. As we move on throughout the rest of the quarter, we'll continue to use these techniques in every language and proof methodology we study!
Week 04 - Imp: Operational Semantics
April 20, April 22 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
Transition systems are a general and flexible technique for modeling the behavior of programs, but manually specifying a transition system for each program we'd like to reason about is tedious and potentially error-prone. Instead, we can use operational semantics to automatically map a program P to its corresponding transition system directly from P's syntax. In particular, we'll see how to do this for the small "Imp" language used to model imperative programs with unbounded loops. In Coq, we'll focus on a fine-grained version of operational semantics called small step operational semantics and in lecture we'll also discuss "pen and paper" versions of alternative styles like big step operational semantics which can make some proofs cleaner or "more natural" but doesn't directly support non-terminating executions.
Week 05 - Hoare Logic
April 27, April 29 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
As we prove more and more invariants for Imp programs, a proof methodology emerges: we can break the overall proof of a bigger program into smaller proofs for each part of the program. It turns out that there's a very nice approach for writing such proofs in a system called Hoare Logic. What's even cooler is that we can prove that any proof we write in Hoare Logic is actually true! This process of proving our proof systems correct is called metatheory and will be a major theme in this week and for the rest of the course!
Week 09 - Compiler Correctness: Simulation Relations
May 25, May 27 : 🧑🏫 Slides · 🧑💻 Code · 📺 Videos
