Seminar for foundations of mathematics and theoretical computer science
Faculty of Mathematics and Physics, University of Ljubljana
CUR - DESIGNING A LESS DEVIOUS PROOF ASSISTANT
William J. Bowman (University of British Columbia)
June 25, 2020
Proof assistant: Cur (github.com/wilbowma/cur)
Dijkstra said that our tools can have a profound and devious influence on our thinking. I find this especially true of modern proof assistants, with "devious" out-weighing "profound". Cur is an experiment in design that aims to be less devious. The design emphasizes language extension, syntax manipulation, and DSL construction and integration. This enables the user to be in charge of how they think, rather than requiring the user to contort their thinking to that of the proof assistant. In this talk, my goal is to convince you that you want similar capabilities in a proof assistant, and explain and demonstrate Cur's attempt at solving the problem.