The 1969 paper An Axiomatic Basis for Computer Programming by C.A.R. Hoare contains one of the first attempts at rigorous reasoning about computer programs. To date, the paper gathered over two thousand direct citations, and many software verification tools, both practical and academic, have been based on the ideas contained in the paper.
Computer programming is an exact science
The paper opens with an important observation:
Computer programming is an exact science in that all the properties of a program and all consequences of executing it in any given environment can, in principle, be found out of the text of the program itself by means of purely deductive reasoning.
The observation holds because of how we construct computers physically: any computer processor that does not execute instructions according to its ``programmer’s reference manual’’ is considered broken 1. I consider it a great failure of our field that after 50 years, this observation of Hoare is true only in principle and not in practice.
In practice, software is so complex that it creates an illusion of not obeying exact rules. Although I believe that people reason about software when writing it – otherwise they would have no way of knowing what to write to achieve their goals – , for verification they almost always resort to dynamic testing. In other words, instead of treating software as scientifically knowable and reason-able, most programmers (including myself) usually treat it either as a simple system with only a few behaviors (those that one explicitly tests), or as a chaotic system about which we can only have probabilistic knowledge. I hypothesize that this ill-treatment of computer systems is the main reason for today’s software reliability and security crisis.
But what if we treat it as if it is not?
On the one hand, when we treat software as being simple and only test it on a few cases that we can think of, it might happen (and in practice, it often happens) that under a different set of circumstances, the system will behave in an unintended way, possibly inflicting harm on data, physical equipment, or people. This unintended behavior may lead some professionals to conclude that software is not knowable, that software bugs are necessary, and that we can only have a probabilistic knowledge of the software we write. Such views are commonly expressed on the web, both explicitly and implicitly.
But on the other hand, if we treat software as a chaotic system, we lend ourselves to security problems. These arise because what a software engineer considers a too chaotic system to handle, an attacker may consider reasonable. This view of mine should not be too controversial because people often say things like “do not write your own hash functions” and “do not roll your own crypto”..
The main contribution of Hoare'69
The paper is constructed around the idea that we can create an exact, axiomatic interface on top of a programming environment (a computer and a language). According to Hoare, we can develop axioms and inference rules for reasoning about software. If the programming language satisfies these rules, then any deductive argument built using them is correct. The main body of the paper then demonstrates how to develop such rules for a simple imperative language.
In Hoare’s deductive system (today commonly known as “Hoare logic”), claims about programs are expressed as triples2
{ P } S { Q }
with the meaning “if the formula P holds in some program state and we execute the program S in it and it terminates, then the formula Q will hold in the resulting state”.
To prove such claim, one uses a deductive system, where there is one axiom schema or inference rule corresponding to every statement of the target programming language. For example, the assignment statement
x := e
(where e is a side-effect-free expression and x a variable)
gives rise to the axiom
.
-----------------------
{ P[e/x] } x := e { P }
(where P[e/x] denotes the result of substituting the expression e for the variable x in the formula P).
All control-flow constructs of the target language are assigned proof rules like that.
Relation to my work
All research around deductive program verification is based on Hoare’s ideas. In the past 10-15 years, there was some work done by Grigore Rosu and people around him that tried to generalize this deductive approach to scale to all programming languages inexpensively - that is, in a way that does not require paying research to conduct new research when a language changes, or when one comes up with a new language. I orient my work (e.g., Cartesian Reachability logic) in the same direction.