u/mttdin r/ProgrammingLanguages • Recommends
"Is it time for a new proof assistant?" - Jon Sterling
0:00 / 0:00
#homotopytypetheory#proofassistant#lean
Jon Sterling, Is it time for a new proof assistant?
HoTTEST
2.8K subscribers • 2 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Jon Sterling
- An opinion. It argues one side of a question engineers disagree on.
Advanced. Deep dive for people who know the field.
5.2K views1 year ago1 recommendation
Programming languagesComputer scienceComputation and complexityFormal methods and verificationLanguage design and type systems
Jon Sterling discusses the potential for a new proof assistant for homotopy type theory, focusing on algebraic hierarchies and user experience.
Homotopy Type Theory Electronic Seminar Talks, 2025-09-25 uwo.ca/math/faculty/kapulkin/seminars/hottest.html It could be time to build a non-experimental proof assistant for homotopy type theory and univalent foundations. I’ll give my thoughts on what that would entail, and where we are able to contribute in the era of Pax Leanica, focusing on algebraic hierarchies, carefully designed user experience, and a proposed return to foundational orthodoxy. --- A message from the speaker: In this talk, I inadvertently referred to Conor McBride with the wrong pronouns. I’m deeply sorry to Conor for this mistake, and also to anyone else who felt alienated as a result. The uploaded slides have been corrected, but the mistake is present in the recording. Sincerely, Jon.Why it's here
1 person recommends thisWhat people say. Recommended as a thought-provoking talk on the future of proof assistants and homotopy type theory.