About the Class

What will it take to build a world in which programmers of all skill levels can formally prove the absence of costly or dangerous bugs in software systems? This seminar will explore technologies for automating formal proofs about software systems in proof assistants like Coq, Lean, or Isabelle/HOL.

Example topics include languages for proof automation, automated theorem proving for proof assistants, plugins and transformations, neural proof synthesis, and usable automation. These topics will be explored through a combination of paper reading and collaborative exploration of code artifacts.

Background in functional programming is expected; background in proof assistants is not needed.

Format

Class Format

The class will meet twice per week. Every one or two week period will explore a particular topic in proof automation. In a typical week, on the first day, we will discuss a paper related to that topic in depth. On the second day, we will collaboratively explore and modify a code artifact associated with that paper. The goal of this format is to really give students a sense of how proof automation works, demystifying what can at times feel like magic.

Some weeks may feature guest lectures in lieu of paper discussions or artifact explorations. The final week will center project proposals by students in the class, with the goal of fostering collaboration.

As this is a graduate special topics seminar, grading will be fairly relaxed (see more below). Students will each be expected to facilitate one paper discussion---this basically just means reading the paper in more depth than other papers, showing up with additional discussion questions, and keeping the conversation going. There will also be very small (less than one paragraph) discussion exercises for each paper and artifact on a class forum. And there will be a project proposal during the last week. The goal is just to learn some cool new things and inspire some cool new projects.

Schedule

Class Schedule

Relative to last semester, this semester, I am planning to spend a bit more time on background information and foundations at the beginning. An outline of the schedule is below. Links are populated with class summaries along with any work due that day. See below for information on how assignments are graded.

Topic Day 1 Day 2
Foundations
Proofs & Logic

Readings this week are optional, but may help with understanding.
08/23/2022
11:00 AM

Read?
08/25/2022
11:00 AM

Read?
Foundations
Types & Curry-Howard
08/30/2022
11:00 AM

Read
Discuss
09/01/2022
11:00 AM

Install
Hack
Motivation
Impacts & Ethics

This week is asynchronous due to AITP.
09/06/2022
Async

Watch
Read
Discuss
09/08/2022
Async

Watch
Read
Discuss
Languages
Tactics

Sign up to facilitate discussions in future weeks!
09/13/2022
11:00 AM

Read
Discuss
Sign Up
09/15/2022
11:00 AM

Install
Hack
Languages
Reflection
09/20/2022
11:00 AM

Read
Discuss
09/22/2022
11:00 AM

Install
Hack
Customization
Custom Tactics
09/27/2022
11:00 AM

Read
Discuss
09/29/2022
11:00 AM

Install
Hack
Plugins
Mixed Methods
10/04/2022
11:00 AM

Read
Discuss
10/06/2022
11:00 AM

Install
Hack
Plugins
Proof Repair
10/11/2022
11:00 AM

Read
Discuss
10/13/2022
11:00 AM

Install
Hack
ATP for ITP
E-Graphs
10/18/2022
11:00 AM

Read
Discuss
10/20/2022
11:00 AM

Install
Hack
ATP for ITP
Hammers
10/25/2022
11:00 AM

Read
Discuss
10/27/2022
11:00 AM

Install
Hack
AI for ITP
Neural Synthesis
11/01/2022
11:00 AM

Read
Discuss
11/03/2022
11:00 AM

Install
Hack
AI for ITP
Autoformalization

Guest: Yuhuai (Tony) Wu (Stanford & Google)
11/08/2022
No Class

Election Day
11/10/2022
11:00 AM

Read
Ask
Human Factors
The Real World

Guest Speaker TBA
11/15/2022
11:00 AM

Read
Ask
11/17/2022
11:00 AM

Install
Hack
Fall Break
Rest
11/22/2022
No Class
11/24/2022
No Class
Human Factors
Social Processes

Get started on your project pitches for next week!
11/29/2022
11:00 AM

Read
Discuss
12/01/2022
11:00 AM

Write
Discuss
What's Next?
Project Pitches

Pitch your ideas and form interest-based teams for the final proposal.
12/06/2022
11:00 AM

Pitch
12/08/2022
No Class

Team Up
What's Next?
Finals Week

Final proposals are due Thursday.
12/13/2022
No Class
12/15/2022
No Class

Submit
Grading

Grading

  • 16 readings at 3 points each = 48 points
    • credit (forum comment) / no credit (no forum comment)
    • first 2 optional (free for everyone)
    • skip any other 2 for free; please ask to skip more
    • automatic credit for the reading you co-facilitate
  • 10 artifacts at 3 points each = 30 points
    • credit (forum comment) / no credit (no forum comment)
    • skip any 2 for free; please ask to skip more
  • Co-facilitation of one discussion at 6 points = 6 points
    • credit / no credit
    • accommodations possible if cannot attend (please ask)
  • One elevator pitch at 6 points = 6 points
    • credit / no credit
    • accommodations possible if cannot attend (please ask)
  • One group project proposal at 10 points = 10 points

Because this is a graduate class, if too many people get below an A in terms of raw grades, I will take this as a sign that I was asking for too much, and scale appropriately.

Free skips: I've added four free skips---two readings and two artifacts. These are just free points in case something comes up, no questions asked. If you need more than this, please let me know and I can accommodate.

Accommodations: Everything is participation-based, but if for personal circumstances you have difficulty participating adequately, let me know and I can accommodate. Life can be tough and I'm not here to make it any tougher. I'm just here to help you make the most of the class. Examples of totally valid reasons to reach out for accommodations: attending a conference, submitting a paper, celebrating a religious holiday, grieving a loss, getting sick, being unable to attend in person due to COVID concerns, disabilities that impact your performance (documented or not), mental health concerns, working a second job, and even just being too tired to get out of bed. I'm happy to have a conversation with you to help you figure out your personal circumstance.

Late policy: Every deadline I've given is a strong suggestion, but I'm not going to penalize you at all if you can't show up to class or if you end up posting your discussion answers late. However, everything must be turned in by the end of the semester, before grades are due. For this reason, I strongly recommend that you adhere to the suggested deadlines unless you need the extra time, otherwise you are likely to regret your decisions later.

Please let me know if you have any questions!