In this paper, he begins with a program written in what I believe to be propositional logic notation. This program can't be typed into an HN comment, but it can be trivially translated in to Common Lisp:
(loop for k from 0 below n always (f k))
The rest of the paper is about him translating this program into another kind of math notation with C-like semantics. By the end of the paper, he has proven that the second, lower-level program is equivalent to the first program, which is the same thing that a compiler does.
He does not prove that the thing he originally wrote at the beginning correctly expresses his intentions. So his method is basically this:
1. Write a bug-free program in a very high-level programming language, or a very rigorous pseudocode.
2. Translate it to a low-level language.
3. Prove that the translation is equivalent to the original program.
https://www.cs.utexas.edu/users/EWD/ewd11xx/EWD1162.PDF
In this paper, he begins with a program written in what I believe to be propositional logic notation. This program can't be typed into an HN comment, but it can be trivially translated in to Common Lisp:
(loop for k from 0 below n always (f k))
The rest of the paper is about him translating this program into another kind of math notation with C-like semantics. By the end of the paper, he has proven that the second, lower-level program is equivalent to the first program, which is the same thing that a compiler does.
He does not prove that the thing he originally wrote at the beginning correctly expresses his intentions. So his method is basically this:
1. Write a bug-free program in a very high-level programming language, or a very rigorous pseudocode.
2. Translate it to a low-level language.
3. Prove that the translation is equivalent to the original program.