Talia RingerOct 29

Next semester I will teach a very experimental class called "Build your own Proof Assistant," in which we come together as a class to build a proof assistant from scratch, targeting some specific set of users (I'm thinking about making it a proof assistant for educational purposes). In doing so we will learn about every piece of the proof assistant, from the foundations to the automation to the interface.

Worst case we learn a lot. Best case we build something useful and get to write a paper about it too.

Show threadTalia RingerOct 29
Thinking of doing something with "language levels" a la @shriramk, but for the amount of automation exposed
Show threadTalia RingerOct 29
Still open to ideas for specific target audiences and use cases. I believe the class will be more successful if we target a specific audience or use case rather than try to build a full general-purpose proof assistant
Show threadBrad Heintz
@TaliaRinger So I'm thinking about this (as a way to procrastinate my automata theory lecture), and every time I think of some field I'd like to play in with a specialty proof assistant, my next thought is, "but first you'd have to implement set theory and (obvs) logic, at least". So if I were setting out on this project on my own, my (likely naïve) intuition would be start with those domains and prove their key results, and then pick a field, bolt its axioms to the side of what I've already built (e.g., Peano for NT) and see what I could build on top of that.
Oct 29 at 6:44pmWeb
Show threadsoaprootOct 29
@bradheintz @TaliaRinger maybe there is a way to use an existing library for set theory? Or use a simple (ish) domain like Peano arithmetic to reduce the size needed? Building a normally capable library of results could be prohibitively time consuming for a class.
Show threadJesper Agdakx 🔸Oct 30
@bradheintz @TaliaRinger You don't *need* any of that for doing more interesting topics. People were doing geometry proofs for thousands of years before set theory was ever invented. It would be very interesting to experiment with bespoke proof assistants that allow for direct reasoning about a specific domain without trying to be general.