Published in Communications of the ACM in 1969, this paper by Tony Hoare argues that the properties of computer programs can be established by formal proof, in the manner of mathematics. It sets out an axiomatic basis for reasoning rigorously about program behaviour.

Central to the approach is a notation, later known as the Hoare triple, which relates a precondition, a program statement, and a postcondition. Hoare presents axioms and rules of inference for basic programming constructs, such as assignment, sequencing and iteration, from which proofs of correctness can be derived.

The paper suggests that such reasoning could improve program reliability and guide the design of programming languages. The framework it introduced, now called Hoare logic, became foundational to formal verification and the study of program semantics.