Edsger W. Dijkstra, the Dutch computing scientist, promoted the development of a program as if it were a proof. He used the notion of the Weakest Precondition (WP) as a mechanism to keep track of your work.
I never wrote a serious program using Dijkstra's method. Little string manipulation exercises fraught with boundary conditions were enough to feel its sweet spots but not enough to generalize to the scale of work I was doing.
I was vaguely familiar with his work from graduate school. I reasoned through synchronization problems using P and V as described in his paper.
Mayer Schwartz had hired one of his students to work in our lab so we picked up some ideas about how big things could be tackled.
The student wrote a syntax-directed editor where he could prove that the program was compile-error free above the cursor. This seemed significant. Later all that checking was ripped out by production programmers trying to get the editor out the door as a product.
The student introduced us to a PhD student of Dijkstra's who came to visit and teach a class.
The five day class was a tour of beautiful programs. Day one was enough Dijkstra-think to appreciate the programs. The remainder were non-trivial programs derived before our eyes as proofs. And yes, they were beautiful.
I was touched by the way WP guided the development of programs. I sought the feel in my Smalltalk work, always moving by small steps thought through and demonstrated by example in a Workspace. Later I saved examples so the experience could be relived. See Automated Testing