It baffles me that the "formal methods" (it really should be called automated methods) crowd not only ignores this lesson, but is completely blind to it. In my direct experience, the ones I've spoken to are so obsessed with verification that the idea of constructing a program that has specified properties apparently isn't even thinkable for them. Perhaps it's a defect in my ability to explain things, but I've never once managed to explain to one of them that construction is a significantly easier task than verification. It's a real shame because they're very intelligent people that I'm certain could contribute greatly to formal program derivation. I suppose it's one of those "professional deformations" Dijkstra occasionally mentions. One of the things I'd like to do when I have copious free time is build an Emacs mode that only allows edits that preserve the given invariants, perhaps using TLA+ or something similar.
Anyone that wants to learn more on the subject of deriving programs should read one or both of A Discipline of Programming[1] and Predicate Calculus and Program Semantics[2]. The former is more approachable for the programmer who isn't as inclined toward formal mathematics. The latter basically takes the same concepts and treats them with much greater mathematical rigor.
[1] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...
[2] https://www.goodreads.com/book/show/3144463-predicate-calcul...
