How do people learn to use interactive theorem provers?

Audrey Seo, Yadi Wang, and Zhennan Zhou. 2022. How do people learn to use interactive theorem provers?. In CSE 510: Advanced Topics in HCI, Seattle, WA. ACM, New York, NY, USA, 19 pages. manuscript, two columns. Best Course Paper 🏆

This is a research project in Paul G. Allen School of Computer Science and Engineering, CSE 510 - Advanced Topics in HCI. We investigated Coq¹, a niche tool in formal verification community. We focus on Coq to demonstrate potential learning barriers and ways to improve its general accessibility and usability for both beginner and more advanced users of ITPs. In this research, we make the following contributions:

• A set of possible learning barriers for interactive theorem provers that will guide future investigations into our main research question.
• Initial findings for improving the overall accessibility and usability of interactive theorem provers, in particular Coq, in the fields of verification and formal methods.
• Additional ideas for tools and resources that beginner-intermediate Coq users might find particularly useful.

Project also credits to: Audrey Seo, Yadi Wang.