Jaro Reinders

Enhancing Interactive Theorem Prover Error Messages with Hints

2026 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

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 …