Hoare Logic

In the AI Story

The triple {P} S {Q} reads: "if P holds before the execution of S, and S terminates, then Q holds after." The precondition P specifies the assumptions under which the program is intended to operate; the postcondition Q specifies the property the program is intended to establish; the program S is the piece of code between them. Correctness is the assertion that for any state satisfying P, executing S produces a state satisfying Q. This is a formal statement; the assertion can be proved or disproved by following the inference rules of the logic.

The inference rules are what make the logic powerful. Hoare gave rules for sequence, assignment, conditional, and iteration — the basic structured-programming constructs — and the rules compose: if you have proved {P} S1 {Q} and {Q} S2 {R}, you can derive {P} S1; S2 {R}. This is the formal expression of the principle that verifications of parts compose into verifications of wholes, which is separation of concerns made rigorous.

Dijkstra's contribution, in his 1975 paper "Guarded Commands, Nondeterminacy and Formal Derivation of Programs," was a reformulation in terms of predicate transformers — functions that take a postcondition and produce the weakest precondition under which a statement is guaranteed to establish it. The reformulation was mathematically equivalent to Hoare's original but better suited to program derivation: the programmer starts with the postcondition and works backward to the precondition, deriving the program along the way. This is the technical machinery of stepwise refinement.

Hoare logic's descendants include separation logic for reasoning about pointer-manipulating programs, concurrent separation logic for reasoning about shared-memory concurrency, and the various formalisms used in proof assistants such as Coq, Isabelle, and Lean. These systems have been used to verify real software, including the seL4 microkernel and the CompCert C compiler — operational demonstrations that Dijkstra's program was not merely theoretical but achievable at industrial scale when the discipline was sustained.

Origin

The foundational paper is Hoare's "An Axiomatic Basis for Computer Programming" (Communications of the ACM, October 1969). The predicate transformer reformulation appears in Dijkstra's "Guarded Commands, Nondeterminacy and Formal Derivation of Programs" (Communications of the ACM, August 1975). Both papers built on earlier work by Robert Floyd on assigning meanings to programs.

The logic has been extended continuously since — separation logic (Reynolds, O'Hearn, Yang, early 2000s), concurrent separation logic (O'Hearn, 2007), refinement calculi (Back, Morgan), and the probabilistic and quantum variants developed in the 2010s and 2020s.

Key Ideas

Triples as formal claims. {P} S {Q} is a precise statement that can be proved or disproved. Correctness is not a vague property but a specific claim.

Inference rules compose. The logic provides rules for combining verifications of parts into verifications of wholes — the formal expression of separation of concerns.

Predicate transformers enable derivation. Dijkstra's reformulation takes postconditions to weakest preconditions, allowing programs to be derived from specifications rather than written and then verified.

Foundational, not obsolete. Hoare logic is the technical backbone of every modern program-verification framework. Its descendants verify real software at industrial scale.

Precise meaning for correctness. Without the logic, "correctness" is a word one gestures toward. With it, correctness is something that can be stated, proved, and checked.

Debates & Critiques

The limits of Hoare logic have been an active research topic for fifty years. The logic works best for sequential, deterministic programs; extensions to concurrency, nondeterminism, and pointer manipulation have required substantial additional machinery. For AI systems whose behavior is statistical rather than logical, Hoare logic applies only to the deterministic components that embed the statistical ones — which is often enough to verify important properties, but never enough to verify the statistical behavior itself. This is the technical reason the verification trilemma bites hardest for AI-era software.