An Early Program Proof by Alan Turing

In order to assist the checker, the programmer should make assertions about the various states that the machine can reach.

the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole programme easily follows.