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


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


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

Comments (3)

  1. The modern name for an ancient programming technique —which roots can be traced back to Dr. E.W. Dijkstra*—

  2. wigahluk says:

    I enjoyed your post; you remained me that, after all this time in programming world, I’m still a mathematician. I’ll read the articles of Dijkstra that you mentioned.

    I’m a little disagreeing with your last point. First, a “formal specification…” can be seen as a test-first programming or test driven development if you think about this formal specification as a unit test written in code, where formality is given by the programming language you are using. If you think about this formal specification as a requirement written in natural language, then the formality is just an illusion and cannot be seen as TDD.

    I believe that you use TDD not for looking for bugs, but for creating bugs. When you write a test before writing the code that passes that test, you are creating a bug that must be corrected,  a mismatch between the system (reality) and your observation (the description you write about this observation: the tests). At the end, you are adapting reality to your observation. That’s the way I prefer to look at “agile” epistemology.

    Happy Holidays!

    Oscar Ponce

Skip to main content