Program Verification: The Very Idea

Abstract

There are those, such as Hoare [20], who maintain that computer programming should strive to become more like mathematics. Others, such as DeMillo, Lipton and Perlis [8], contend this suggestion is mistaken because it rests upon a misconception. Their position emphasizes the crucial role of social processes in coming to accept the validity of a proof or the truth of a theorem, no matter whether within purely mathematical contexts or without: “We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem” [8, p. 271]. As they perceive it, the situation with respect to program verification is worse insofar as no similar social process occurs between program verifiers. The use of verification to guarantee the performance of a program is therefore bound to fail. Although Hoare’s work receives scant attention in their paper, there should be no doubt that his approach — and that of others, such as E. W. Dijkstra [10], who share a similar point of view — is the intended object of their criticism.

I hold the opinion that the construction of computer programs is a mathematical activity like the solution of differential equations, that programs can be derived from their specifications through mathematical insight, calculation, and proof, using algebraic laws as simple and elegant as those of elementary arithmetic.

C. A. R. Hoare