Subscribe to Events

Whenever someone builds a sufficiently complex system, they need to check that it does what they intend. Some aspects of system behavior are so important that their developers write proofs to show that they are correct. This kind of proof work can be essential. But it is also grueling. Could we give people better tools to establish soundness of systems and understand the formalisms that model them? In this talk, I share a modern vision for user interfaces that serve as partners in making and understanding proof. The foundation is recent research from my group on the usage of modern proof assistants. The building blocks are a set of prototype interactive systems we have developed for automated testing, math authoring, and program QA. Together, these components help to outline how future proof tools can assist in checking complex systems and understanding the formalisms they draw on.