3 ms·
That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs: Calculational, structured, and declarative proofs
by cpitclaudel 6y ago
That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs:
Calculational, structured, and declarative proofs
The tactic-based proof style pioneered by LCF [LCF+Gordon1979] is sometimes called *imperative* or *procedural*, in contrast to the *declarative* style introduced by Mizar [Mizar+Trybulec1985] and later implemented in proof assistants like HOL88 [MizarHol+Harrison1996], Isabelle/Isar [Isar+Wenzel1999], TLA+ [TwentyFirstCenturyProof+Lamport2012], HOL Light [MizarLight+Wiedijk2001]_ and even in program verifiers like Dafny [Dafny+Leino2014].
Declarative proofs tend to more closely mirror pen-and-paper proofs, and are generally more readable in isolation than plain imperative proof scripts. They derive from *structured calculational* proofs [ShapeOfArguments+VanGasteren1990, PredicateCalculus+Dijkstra1990, StructuredCalc+Back1997, StructuredHOL+Grundy1997], in which calculations (sequences of propositions chained by logical connectors, each annotated with a succinct justification of the corresponding step, as in `A = { because X } B ⇒ { because Y } C`) are structured through logical cuts and typographical means such as indentation and explicit nesting marks.
A declarative proof language was added to Coq in version 8.1 [Czar+Corbineau2008]_(2006), but it saw only limited use and was removed in version 8.7 (2017). Coq 8.4 instead introduced structure to imperative proof scripts using bullets and braces, giving scripts most of the *structured* part of *structured calculational* proofs. While it is possible to emulate the *calculational* part in imperative proofs using tactics to re-state the current goal and hypotheses after each step in a chain of rewrites, this “checked comments” style is not particularly common in Coq (rich tooling existed in Isabelle to support this style of proofs before the introduction of Isar and the switch to declarative style [ProofPresentationIsabelle+Simons1997]). Alectryon's automatic annotations, combined with careful structuring of proof scripts and judicious use of logical cuts (`assert … by …` or SSReflect's `have`), offer the readability benefits of declarative proofs without the burden of adding output annotations.