I'm not sure. Dijkstra, despite his somewhat incorrect reputation as a curmudgeonly theorist who preferred pencils to computers, had a notable pragmatic streak.

I'm not sure. Dijkstra, despite his somewhat incorrect reputation as a curmudgeonly theorist who preferred pencils to computers, had a notable pragmatic streak. And, as a matter of pragmatism, he identified the close relationship between programs and proofs. There are many such examples in his writings, but here are a few[1][2][3][4]. It's particularly interesting to see how his thinking evolves. EWD288 in particular includes what I view as both good advice and a powerful refutation of a fallacy that is stubbornly popular even today: Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. I have myself applied this in "real" (aka, I got paid for it by a FAANG) programming by proving the correctness of the overall structure of a service (and verifying it with tests) while leaving implementation details for which requirements were nonexistent or unclear unspecified or underspecified. Since I'm neither as creative nor as clever as Dijkstra was I still like to write tests, but I've found that I can do TDD in a way that meshes cleanly with his program and proof construction style. The end result is I have code that I have both proved correct and that has solid test coverage. The tests are particularly useful for collaboration, because it's just not realistic to expect every team member who touches a piece of code to understand and rederive the appropriate parts of said proof. And as an added bonus, it escapes the common complaint for TDD that the tests get in the way of development. They don't when you only test what needs to be proved! Edit: I find it amusing how much closer Dijkstra's approach is to what might be called "normal" (Algol-ish) programming compared to the Abstract Nonsense[5] favored by the category theorists. I wouldn't call it any less mathematical though. Dijkstra was very much a mathematical formalist as is clear to anyone who has made a study of his work or life. [1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD288.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD375.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E... [3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD803/EWD803.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E... [4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/EWD1157.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E... [5] https://en.wikipedia.org/wiki/Abstract_nonsense https://en.wikipedia.org/wiki/Abstract_nonsense