Here’s a passage I wrote in a recent draft:
The tactic-based proof style pioneered by LCF [Gordon1979] is sometimes called imperative or procedural, in contrast to the declarative style introduced by Mizar [Trybulec1985] and later implemented in proof assistants like HOL88 [Harrison1996], Isabelle/Isar [Wenzel1999], HOL Light [Wiedijk2001], and even in program verifiers like 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 [VanGasteren1990, Dijkstra1990, Back1997], in which calculations (sequences of propositions chained by logical connectors, each annotated with a succinct justification of the corresponding step, as in A = \{ \text{because } X \} B ⇒ \{ \text{because } Y \} C) are structured through logical cuts and presentational means such as indentation and explicit nesting marks.
A declarative proof language was added to Coq in version 8.1 [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 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 [Simons1997]). Automatic annotations, combined with careful structuring of proof scripts and judicious use of logical cuts (
assert … by …or SSReflect’shave), offer the readability benefits of declarative proofs without the burden of adding output annotations.
(I can provide the actual references if you’re interested)
The automatic annotations that I’m referring to are a style in which you automatically augment a proof script with the corresponding goals; you can see what it looks like in our lab’s blog (see this announcement: PLV has a new blog! - #2 by Blaisorblade). The case I’m making is that if you have these annotations and you’re careful about using bullets and cuts the distinction between declarative and imperative proofs isn’t big. This point is quite similar to what @Zimmi48 says here: