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 threadRob Rix
@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.
Oct 29 at 10:20pmWeb
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.