The idea that you should design programs with proof in mind goes back to T. J. Dekker's solution to the mutual exclusion problem in 1959. The story is told by E

The idea that you should design programs with proof in mind goes back to T. J. Dekker's solution to the mutual exclusion problem in 1959. The story is told by Edgser Dijkstra in EWD1303 (https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1303.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...). Much of Dijkstra's later work can be seen as him working out the consequences of this insight.