Proofs as programs

Reviewer: Ali Mili

Bates and Constable discuss the use of constructive proofs as a paradigm for programming. They introduce an implemented program development system, called PRL, that is based on this paradigm. The use of PRL is illustrated on a programming problem, that of finding a consecutive subsequence of maximum sum in a finite sequence of integers. The basic thesis of the paper, constructive proofs as programs, is quite appealing, and the authors present it in a lively—perhaps opinionated—manner. Also, this reviewer finds the discussions in Section 2 on mathematical problemsolving and its relevance to programming to be interesting and thought provoking. Finally, system PRL does appear to be useful, though this reviewer does not know enough about other systems to confirm the claims made for this one. The reader might be annoyed by the expediency with which some controversial statements are made. An example of such is the statement that “comments, written in pidgin English, attached to the code. . .are not the way to explain a program.” Another example is the statement that a program carries “no trace” of the “intellectual effort that went into producing it." Without expressing opinions on them, this reviewer merely suggests that these are controversial statements that need to be made with some care. On balance, this paper (and its extensions, as seen in the bibliographic references) is very useful to anybody doing research on program construction. It is also quite readable.