2026-08-24T11:05:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26979 2026-07-16T09:49:33Z ddc:004 open_access

Enhancing Interactive Theorem Prover Error Messages with Hints Khakimova, Maria Juhošová, Sára Reinders, Jaro Cockx, Jesper Agda error messages hints new users Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP’s underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Maria Khakimova and Sára Juhošová and Jaro Reinders and Jesper Cockx 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.5 urn:nbn:de:0030-drops-269791 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.5 eng https://creativecommons.org/licenses/by/4.0/legalcode