Dijkstra once explained what he meant when he claimed you could "derive" correct programs mathematically: https://www.cs.utexas.edu/users/EWD/ewd11xx/EWD1162.P

Dijkstra once explained what he meant when he claimed you could "derive" correct programs mathematically: https://www.cs.utexas.edu/users/EWD/ewd11xx/EWD1162.PDF 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.