CSCI 1951x

Formal Proof and Verification

Fall 2024

Welcome to CSCI 1951x at Brown University!

IMPORTANT NOTE FOR FALL 2024 REGISTRATION: This course is open to math majors. To request an override for CS1951x, please use the central override form provided by the CS department, even if you are not a CS major. Do not email Rob or the CS1951x staff. Direct questions or concerns about the course override process to enroll-questions@lists.cs.brown.edu.

Course Description

Proof assistants are tools that are used to check the correctness of programs. Unlike tools like model checkers and SAT solvers, proof assistants are highly interactive. Machine-checked formal proofs lead to trustworthy programs and fully specified reliable mathematics. This course introduces students to the theory and use of proof assistants, using the system Lean. We will use Lean to verify properties of functional programs and theorems from pure mathematics. We will learn the theory of deductive reasoning and the logic that these tools are based on.

Syllabus: syllabus.pdf

Lecture: MW 9:30–10:50 a.m., CIT 241

Lab: Th 4:00–6:00 p.m., CIT 348

Course Content

We plan to cover most of the Hitchhiker’s Guide to Logical Verification. We'll cover chapters roughly according to the schedule below, but topics may shift slightly as the semester progresses.

Assignments

Homework

Homework will be submitted via Gradescope. Please ensure that you have familiarized yourself with the grading and collaboration policies in the syllabus.

Homework Material Covered Released Due
HW 0 A quick survey 9/4/24 9/11/24
HW 1 Ch. 1, 2 9/9/24 9/18/24
HW 2 Ch. 3 9/16/24 9/25/24
HW 3 Ch. 4 9/23/24 10/2/24
HW 4 Ch. 5 9/30/24 10/9/24
HW 5 Ch. 6 10/7/24 10/18/24
HW 6 Ch. 9 10/22/24 10/30/24
HW 7 Ch. 13 10/28/24 11/6/24
HW 8 Ch. 12 11/4/24 11/13/24

Labs

Labs are optional, TA-guided sessions that provide an opportunity to practice and reinforce the content covered in lecture. Labs are held every Thursday, 4:00–6:00 p.m. in CIT 348.

Lab Date
Lab 1 (Lean Basics) 9/12/24
Lab 2 (Backward Proofs) 9/19/24
Lab 3 (Forward Proofs) 9/26/24
Lab 4 (Functional Programming) 10/5/24

Lectures

You can view lecture demo files and view lecture recordings here. We will aim to update this table shortly after each lecture. All lecture recordings can also be found on Panopto.

Date Topic Resources Summary
9/4 Introduction Recording
Ch. 0 notes
We'll talk about what Lean is and see what it can do, and also go over some organizational points about the course.

Takeaways: Verified programming is fun and powerful!
9/9 The basics of Lean syntax Recording
Ch. 1-2 notes
In this lecture we'll learn the basics of the Lean programming and specification language: types and terms, type inhabitation, and writing and evaluating very simple functional programs. No proving yet!"
9/11 Dependent type theory Recording
Ch. 1-2 notes
We'll finish Chapter 2 of the HHG, and get a head start on some material from Chapter 4. Today's topics: inductive types (continued), function definition and evaluation, specifications, and dependent type theory.
9/16 Backward (tactic) proofs Recording
Ch. 3 notes
We'll dive into the meat of the HHG Ch. 3: what are some of the moves available to us in the tactic proving minigame, beyond intro and apply? How do we deal with logical connectives: And, Or, Not, and so on?
9/18 Backward (tactic) proofs, contd. Recording
Ch. 3 notes
We'll continue talking about tactic proofs. How do we deal with equality? What about the natural numbers? We'll also talk about classical vs constructive logic.
9/23 Forward proofs Recording
Ch. 4 notes
We'll see another way to write proofs in Lean, incorporating forward reasoning. Structured ("proof-term") proofs are a little closer to the underlying logic. Surprise: proofs in Lean are, literally, just terms in the type theory.
9/25 Dependent types Recording
We talked about dependent types before; now, more. The type theory that Lean is based on, the Calculus of Inductive Constructions, is an instance of dependent type theory. In DTT, we follow the PAT principle: propositions as types, proofs as terms. (Buzzword: the Curry-Howard correspondence!) We'll look deeper today into these foundations. Time permitting, we'll look at a few important algorithms, including unification.
9/30 Functional programming: data structures Recording
Ch. 5 notes
Chapter 5 of the Hitchhiker's Guide introduces some paradigms — inductive types, structures, recursive definitions, type classes — that might be familiar from other functional programming languages. The interesting thing for us is how these paradigms interact with writing proofs. For instance, how do we mix properties into data structures?
10/2 Functional programming: type classes, lists, trees Recording
Type classes are a language feature inspired by Haskell with equivalents in Scala, ML, and other languages. They allow us a kind of ad hoc polymorphism: we can define functions on types that implement certain interfaces, and can declare that certain types implement these interfaces, without bundling the interfaces into the data type itself. we'll see how this interacts with some of the data structures we like to use, as we implement and specify functions on these types.
10/7 Inductive predicates Recording
Ch. 6 notes
We'll cover ch. 6 of the Hitchhiker's Guide today, on inductive predicates. This will complete what we need to know about foundations for now: inductive predicates give us a way to introduce new propositions and prove things about them. Inductive predicates are also the source of most of the propositional symbols we've used so far — And, Or, Exists, Eq, ….
10/9 Big-step operational semantics Recording
Ch. 9 notes
We're jumping ahead to Chapter 9 today! Time to start putting what we've learned into practice. We'll define the syntax of a toy programming language inside of Lean, discussing the difference between shallow and deep embeddings. Using inductive predicates, we'll define a transition system and use this to prove things about the execution of programs in this toy language.
10/16 Small-step operational semantics Recording
The big-step semantics we saw on Monday aren't fine-grained. We can't reason about intermediate states. An alternative is using a small-step semantics, where our program execution path is broken down much further. This comes with upsides and downsides.
10/21 A look under the hood Recording
Ch. XX Notes
We'll talk theory today, about the data structures and process flow that underlie a proof assistant. Basically, we'll think about Lean as a programming language in the sense of the last two lectures. What's its syntax? What are its semantics??
10/23 Logical foundations Recording
Ch. 12 Notes Russell's Paradox
As this course has progressed, we've gotten some insight into the foundations of Lean and its type theory. But some features have remained mysterious. In the next few lectures we'll poke some more at this foundational theory. Today we'll be focusing in particular on the type universe Prop, what we're allowed and disallowed in this universe compared to the others.
10/28 Algebraic structures Recording
Ch. 13 Notes
We'll jump ahead again to chapter 13, where we'll start talking about algebraic structures. But we'll also improvise a bit here. After we see some basic structures, we'll define some mathematical types of our own.
10/30 Numbers and sets Recording
We'll continue the Ch 13 material we started last time, including a little more with the complex number playground. We'll also talk about embeddings between different numerical structures, and some different kinds of "set-like" objects.
11/4 Logical foundations, contd. Recording
We'll continue with chapter 12 today, talking about more foundational constructs. As we discussed last class, there's a grab bag of features that we can take or leave: proof irrelevance, impredicative Prop, the axiom of choice, and others. Why should we be convinced that the collection we choose is consistent? We'll introduce the notion of a model of the type theory to answer questions like this.
11/6 Quotients, rationals, and reals Recording
The last bit of Ch. 12, on quotient types, is very relevant to what we want to do next! We'll wrap up that discussion (including talking a bit about the computability properties of quotients) and then immediately use quotient types to define some familiar things. Rational and real numbers are interesting mathematically, and for programming purposes, they can be a very convenient tool for writing specifications. Even if we don't compute with real numbers they're useful to have around.
11/11 Real numbers Recording
We finished last week with the rational numbers. Now we need to complete them to get the reals. This will take yet another quotient. The reals bring to light some computability issues that we've touched on briefly before: what does it mean to compute with real numbers? How do we do it in normal languages? If time permits, we'll look at mathlib's implementation of the reals and see some generalizations.
11/13 Monads and tactics Recording
Lean has a very powerful framework for writing custom tactics. These tactics are written in Lean itself, with a number of catches to make this possible. Today we'll see the fundamentals of this approach. We'll learn the (very) basics about monads, a technique used in some functional languages to simulate programming with side effects. (But this isn't an FP class and we're not going to dwell on monads, beyond what we need to know.) Chapter 7 of the HHG is a more detailed introduction to monads.
11/18 Monads and tactics Recording
More from chapters 7 and 8 of the HHG. We'll look at macros, a simple kind of metaprogram. Then we'll turn our attention to the TacticM monad, which provides an API for interacting with our context and goals.
11/20 Monads and tactics Recording
We'll continue our discussion of metaprogramming by implementing a few custom tactics. Along the way, we'll see some more metaprogramming techniques and a few "imperative-like" features of monads that make our lives easier when writing tactics.
11/25 Monads and tactics Recording
Metaprogramming TBD
12/2 Guest lecture TBD Recording
12/4 Tactic design strategies Recording
The tactics we've seen so far manipulate the tactic state in stages. Today we'll consider some high level designs for automation: proof by certificate and proof by reflection. We'll also talk about the strategy and algorithm behind the tactic linarith, a great example of a "large" metaprogram that shows off a number of interesting design principles.

Calendar

Resources

Course Links

Lean Documentation & Search Tools

Lean Manuals

Community Resources

Staff

To email the course staff, click here. To email just the HTA and Rob, click here. To email Rob directly, click here. You are also encouraged to post (and answer!) questions on Ed Discussion.


Photo of Robert Y. Lewis

Robert Y. Lewis

Professor

Call me Rob! I'm half computer scientist, half mathematician, and fully excited to go through some of my favorite material with you all this semester. Pronouns: he/him/his

Photo of Komron Aripov

Komron Aripov

HTA

Hi guys! At Brown, I'm interested in operations research, formal methods and more. You can find me sipping matcha in Ceremony or working on my next project in the BDW. Ask me anything about 3D printing and electronics :) Pronouns: he/him/his

Photo of Chloe Qiao

Chloe Qiao

UTA

Hi, I'm Chloe! I like formal methods, systems, and most things in-between. When I am not hanging out at the Sunlab, I can be found climbing or playing Dance Dance Revolution. It's my pleasure to be your UTA this semester! Pronouns: she/her/hers