Although my own previous enthusiasm has been for syntactically rich languages like the Algol family, I now see clearly and concretely the force of Mi… - Robert W. Floyd

If I ask another professor what he teaches in the introductory programming course, whether he answers proudly "Pascal" or diffidently "FORTRAN," I know that he is teaching a grammar, a set of semantic rules, and some finished algorithms, leaving the students to discover, on their own, some process of design.

A semantic definition of a particular set of command types, then, is a rule for constructing, for any command of one of these types, a verification condition on the antecedents and consequents.

The establishment of formal standards for proofs about programs [...] and the proposal that the semantics of a programming language may be defined independently of all processors for that language, by establishing standards of rigor for proofs about programs in the language, appears to be novel.