Enhancing Proof Assistant Error Messages with Hints: A User Study

Maria Khakimova

Proof assistants are tools that allow programmers to write formal proofs. However, despite the improvements made in recent years, there is still a limited amount of published user studies in improving the usability of dependently-typed proof assistants. This is especially true for investigating the effects of enhancing error messages on novice programmers, even though it is a popular topic for imperative languages.

This thesis aimed to help fill this gap in knowledge by using Agda as a research vector. We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students to determine the effects that these error messages had on the usability of Agda.

Results show statistically significant improvements in the number of compiling submissions, and the rated “helpfulness” of the error messages (when compared to the original messages without hints). However, we were not able to determine if there was any statistically significant impact on the overall speed at which students resolved the errors. Furthermore, while we identified decreases in the ratings of “incorrect” hints, they did not appear to significantly influence the success rate, or time taken to fix an error. We concluded that enhancing error messages with hints is a promising avenue for improving the usability of dependently-typed proof assistants.

---

Previous: Pim Otte | Waterproof: Demo of an educational tool built on a theorem prover
Next: