Lab Lunch: 19 January 2021 - Liam O'Connor

Title: A Chronology of Proof Assistant Attempts

Abstract:

“Every now and then I feel a temptation to design a new [proof assistant] but then I just lie down until it goes away.” - L. Peter Deutsch (paraphrased).

Since I first began using a proof assistant I’ve seen their potential utility for education. At UNSW I taught a programming languages course and formal methods courses that had students doing pen-and-paper proofs, but their mathematical arguments were often unconvincing at best. A mechanical proof assistant can provide earlier and faster feedback than I can, and ensures soundness of their proofs. Benjamin Pierce and others successfully used the Coq proof assistant with the Software Foundations book to teach similar material[1], and Phil Wadler uses Agda here at Edinburgh, but I am more interested in designing a bespoke proof assistant specifically for the educational use-case.

In this talk, I will talk about this goal and my rationale for it, my various failed attempts and false starts at achieving it (including some demonstrations), and Holbert: the latest iteration of this idea that is still under development. Holbert is a higher-order logic proof assistant with a graphical interface than runs in the browser. I hope to get some feedback on its design as well as to generate some enthusiasm for the project.

Dr. Liam O’Connor, Lecturer in Programming Languages for Trustworthy Systems.

[1] Pierce. "Lambda the Ultimate TA”, in ICFP 09  doi 10.1145/1596550.1596552