How Novices Perceive Interactive Theorem Provers (Extended Abstract)
summary
Survey of 35 bachelor students who learned Agda for two weeks finds five concrete obstacles: unfamiliar concepts (dependent types and proof-centric workflow), steep and abstract theory, and weird design such as mandatory Unicode, spacing-sensitive syntax and opaque error messages. The tooling is an inadequate ecosystem: Agda-mode on VS Code crashes, syntax highlighting disappears, documentation omits basic semantics. Only one student had prior ITP experience, and conclusions call for sturdier, novice-oriented infrastructure and clearer, example-driven core docs.
AI-written summary · about
chapters (12)
- 0:00Novice struggles with theorem provers
- 2:18Study goals and approach
- 3:00Study setup with students
- 4:47Qualitative research methods
- 7:16Five obstacles with ITPs
- 11:11Agda’s usability observations
- 12:34Conclusions and future directions
- 13:39Future projects and improvements
- 14:06Q&A: Language design vs usability
- 15:29Q&A: Tools for students and Unicode
- 18:56Q&A: Prerequisite skills
- 20:44Q&A: Agda’s perceived irrelevance
related talks
01h 01mDeclarative Programming and Education
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
19mQED in Context: An Observation Study of Proof Assistant Users
15mOn the Impact of Formal Verification on Software Development
19mUsability Barriers for Liquid Types
29mType Inference Techniques: Implementation and Formalization, Better Together
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
16mIncremental Proof Development in Dafny with Module-Based Induction