Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Yuhui Lin, Gudmund Grov, Rob Arthan

TL;DR
This paper explores the use of a graphical language, PSGraph, to represent proof strategies in theorem proving, demonstrating improved understandability and maintainability over traditional linear tactic languages.
Contribution
It extends PSGraph with new features for development and debugging, and compares its effectiveness to linear tactic languages through re-implementation of existing tactics.
Findings
PSGraph improves debugging and readability of proof tactics
Refactoring tactics in PSGraph enhances maintainability
Graphical representation aids understanding of complex proof strategies
Abstract
The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst being elegant, the use of higher order features and combinator languages often results in a very procedural view of a strategy, which may deviate significantly from the high-level ideas behind it. This can make a tactic hard to understand and hence difficult to to debug and maintain for experts and non-experts alike: one often has to tear apart complex combinations of lower level tactics manually in order to analyse a failure in the overall strategy. In an industrial technology transfer project, we have been working on porting a very large and complex proof tactic into PSGraph, a graphical language for representing proof strategies, supported by the Tinker tool. The goal of this work is to improve…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsTeaching and Learning Programming · Software Testing and Debugging Techniques · AI-based Problem Solving and Planning
