Talia Ringer

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.

Oct 29 at 6:08pmWeb
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 threadYotam DvirOct 29

@TaliaRinger Wow, ambitious, good luck! Would have loved to be a student in such a course.

"For educational purposes" is pretty broad. I'll just say that I always wished, as a tutor of incoming undergrads, for a proof assistant that can help students structure their epsilon-delta calculus proofs. That way the computer can catch their nonsense while they are producing it, rather than the person grading their assignments. Getting rid of the feedback delay would be extremely helpful, I think.

Show threadBrad HeintzOct 29
@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.
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.
Show threadRob RixOct 29
@TaliaRinger I’m building a constraint solver for CAD software, and solving metas in algebraic expressions feels a bit like higher-order unification in places. It actually helped me understand the latter better, and also normalization by evaluation. And I’m planning to rewrite the solver around a tactic language! Dunno if any of that is helpful.
Show threadBrendan ZabOct 30
@robrix @TaliaRinger Would _love_ to hear more about this. Been trying to bring my PL stuff back to geometry land (which was always my hope) and it can be a struggle.
Show threadRob RixOct 30
@brendan I’m having trouble writing my thoughts up. Want to do a video call sometime? I’d find it valuable to figure out what’s even worth talking about here, which might in turn help me write a blog post or something.
Show threadShriram KrishnamurthiOct 29
@TaliaRinger Emailed you…
Show threadBrad HeintzOct 29
@TaliaRinger This sounds super cool and I am envious of your students!
Show threadBrad HeintzOct 29
@TaliaRinger (Checking the drive from Indy to U-C...)
Show threadDavid YoungOct 29
@TaliaRinger Sounds fun! I would have loved to take a class like that