Once we have accepted that the significant effort in programming is not coding but problem solving, we naturally recognize the necessity of formalizing the entire activity of program derivation. First, we need a formal specification language, and there are obvious advantages in having uniformity of language for expressing both specifications and programs. There are many proposals that meet this requirement. In fact, it is carried to an extreme in Prolog, where specifications are even executable.

In this paper, which may be seen as an extension of [1], the authors choose Predicate Logic as the uniformizing language. They then show how the usual high-level program notations can be viewed as abbreviations for predicates that are particular, in that they are proved satisfiable by implementation. This allows them to identify program derivation with the construction, step by step, via the rules of Predicate Calculus, of the formal proof that the specification is implementable. But the enormous amount of detail is often a serious obstacle and causes many to reject formality.

“Mathematicians do not always prove a theorem from axioms;” a large stock of definitions, theorems, and proof techniques, which are the result of a long series of preceding experiences, helps them. Analogously, programmers should be able to formalize their “know-how” or “program paradigms” that allow them to avoid always starting from scratch.

The paper reviewed moves in this direction. A number of useful theorems are reported that serve for deriving example programs. I hope many others will follow this path, not necessarily with the same formalism but with the same aim.

The paper is clearly written and well organized. Everyone who thinks that a correct program activity is not too far from (constructive) mathematics should find it interesting and stimulating.