The use of tactics in modern proof assistants seems to have the same flavor of usability problem as trait errors. For example, a programmer applies a tactic to some goal; the application either succeeds or gets simply a “No” failure. In theory, similar techniques might be useful to diagnose a trait error as to diagnose a tactic failure. However, we struggled to find much related work on this subject. In the space of proof assistants there are two styles of tool, proof visualizers and proof state visualizers. The former emphasizes writing proofs, following a pattern similar to that taken on paper, and the latter emphasizes understanding the state of the current proof.
Proof state visualizers render the proof tree before and after each tactic application, but do not help with understanding the application itself. Notable tools in the space include Alectryon 26 for Lean and Coq-PSV 12, and Shi et al.2023 describe a “tactic preview” which can help readers of proofs identify the goals solved by a given tactic. Even though proof state visualization may seem tangential to trait solving, an extension for Argus is to iteratively step through the solver’s execution visualizing the type state at each step. We imagine this feature would be more useful to compiler writers and library maintainers.
Proof visualization tools seem to take an approach of modeling sequent calculus with Gentzen trees. These tools aim to help proof writers by providing a more “paper-like” feel to mechanized proofs. The oldest tool in this space, ProofTree, works with Coq and ProofGeneral and displays the tree top-down similar to the Argus And–Or tree.
