Hoare Logic, Pascal P, and Kesav Nori

Here is a short description of how Prof. Kesav Nori used Hoare logic, in his own words:

"I do not recall what I told you about Hoare logic, but in order to prove correctness of the Pascal P compiler, I proposed Axioms a la Hoare Logic for each P-code instruction (including jumps and conditional jumps) and the rule of inference for sequential composition, and then showed that every axiom and rule of inference of Pascal P was a theorem for the compiler geberated code schema. This way, any proof of a program property for a Pascal Program could be treated as a proof for the generated P code, citing the code generation theorems, and that would be a means of asserting semantic preservation, i.e., a compiler is a bridge between two proof systems, respectively for the source and target languages. Hoare logic (or any specification language for semantics of a Programming Language) is a meta language in which the bridge can be specified."

"... it was clear as mud, but it covered the ground ..." !