The Professor Edsger Wybe Dijkstra school of thought

I have been reading some manuscripts of Edsger Wybe Dijkstra. He said several years ago that the nature of the programming task implies a sound background on mathematics and applied logic in order to programmers do a really good job.

Take note, mathematics as “…a human activity, with patterns of reasoning, with methods of exploiting our powers of abstraction, with traditions of mixing rigor with vagueness, with ways of finding solutions. It is in this second meaning that I judge mathematics as highly relevant for the programming task”

-On a methodology of design

https://www.cs.utexas.edu/users/EWD/ewd03xx/EWD317.PDF

Also he said that “Being a better programmer means being able to design more effective and trustworthy programs and knowing how to do that efficiently. It is about not wasting storage cells or machine cycles and about avoiding those complexities that increase the number of reasoning steps needed to keep the design under strict intellectual control. What is needed to achieve this goal, I can only describe as improving one’s mathematical skills, where I use mathematics in the sense of ‘the art and science of effective reasoning’. As a matter of fact, the challenges of designing high-quality programs and of designing high-quality proofs are very similar, so similar that I am no longer able to distinguish between the two: I see no meaningful difference between programming methodology and mathematical methodology in general. The long and the short of it is that the computer’s ubiquity has made the ability of apply mathematical method more important that ever.”

-Why American Computing Science seems incurable

https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1209.PDF

Later I recall those formal methods like VDM and those using Z notation which include mathematic formality for software specification and design, so I review some introductory papers (J.A. Hall, Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990) about these formal methods and found many similarities with eXtreme Programming practices, specially, test-first programming (or test-driven design), for example:

“A formal specification is a precise definition of what the software is intended to do” – isn’t the spirit of test-first programming?

“[formal specification] is concerned only with the function of the system and makes no commitments to its structure” – at unit tests level, the ‘function of the system’ becomes ‘function of the type/class/module’, isn’t?

“Instead, you construct a correct program in small steps. Each step takes the specification and produces something a little nearer to the final program. Each step is small enough that you can see exactly what needs to be proved to show that the step is correct.” – aren’t the eXtreme Programming test/code/refactoring micro-cycles? Practitioners of formal specification methods like VDM would enjoy eXtreme Programming.

Test-driven development is a best-of-breed design technique.

Also, from the same school of thought, David Gries said:

"We should run test cases not to look for bugs, but to increase our confidence in a program we are quite sure is correct" -The science of programming. 1981 Springer-Verlag