Proof Automation

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.

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.

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.

• 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
  • see rubric for details
  • accommodations possible if needed (please ask)

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!