An analogy between computer programs and mathematical proofs

Dated: 

November 1981

In 1961, Dijkstra made an analogy between mathematical proofs and computer programs. After noting the analogy, he took aspects from the field of mathematics and projected them onto his own profession of programming.

Twenty years later, Dijkstra still stood by the analogy. This time, however, he projected the lessons he had learned from programming methodology back onto mathematics. Dijkstra was thus, in 1981, keen on defining a mathematical methodology. In Dijkstra's words:

I am relying on the analogy between programs and proofs, an analogy which is the inspiration behind my effort to transfer what programming methodology has taught us to mathematical methodology in general.

To further clarify his research agenda, Dijkstra distantiated himself from dominant traditions in logic, philosophy, and mathematics. Dijkstra was not interested in formalisms for the sake of capturing the foundations of mathematics. Instead, he only wanted to use formal methods if they could help pragmatically; that is, if they could help in conducting mathematics itself.

Dijkstra knew that his unorthodox research agenda would be countered by dominant voices. He therefore stressed from the start that he did not expect others to share his interests.

We are not prescribing the law to anybody, we are not even attempting to propose something, but have rules for ourselves.

Source: the first few pages of EWD 803.

Tags: 

5 Comments

Imperfect people

Funny, but being more a generalist than a specialist, the fact that even smart people, experts in their domain, are not open to views coming from other domains is everywhere. Scientists are in this respect as imperfect as anybody else.
The reason is that our brains only get better by being trained. Training in the large sense means like a neural network. The more stimuli of a certain kind you give it, the better the "pattern recognition" starts to work. At the same time, this makes the brain rigid like in "brainwashing". We become blind at recognising new patterns.
Progress, creativity, insight often comes from being able to color outside the lines, from being able to see a common pattern between seemingly different things (the Aha-reaction). Forcing oneself to look for a meta-meta-... model can help because it is a thinking technique that abstracts away from the details and it is one at the essence of mathematical thinking.
This also highlights (again!) the importance of a good and open education. In our fast evolving world, we should learn skills (like using a tool) but also the skills to learn and seek something new. This is a long term effort as once the brainwashing has set in, it is very hard to reverse it. If then combined with a bureaucratic system of getting funding for e.g. research and teaching, it is a recipe for wasting a complete generation. This translates into lost wealth and economic freedom as we see today.

Dijkstra doesn't like metaphors or analogies

Again Dijkstra is contradicting himself. In one or more of his EWD articles, he criticizes analogies heavily because he thinks that radical novelties (like programming) cannot be compared to existing things. Please post the EWD if you know which one it is. So here Dijkstra is using an analogy, even though he is hostile toward analogies..

Here is a proof why programming is not math (it is a combination of math, engineering, design, and art):
A GUI program can have artistic qualities to it. Even a console program can. A button can be colored red, gray, or blue. There is no way to mathematically prove that a GUI program is correct, you can only prove some of the program correct (can't prove the design/art parts correct). Therefore programming is not the same as math. Programming contains math, but programming is not math.

How could you prove that a button in a gui should be a certain width? A button could be 60 pixels or 50 pixels and it could be red or blue or another color. It depends on the taste/art/style of the GUI. These algorithms modifying the GUI cannot be proven correct. However other algorithms such as whether or not certain tokens exist in a string, can be proven correct (a loop can be proven to continue to infinity which is a program bug).

Response to PracticalID

I don't think you understand what it means to prove a program correct. (I suggest you study what Dijkstra wrote.) On why your "challenge" about the width of a GUI button misses the point, see EWD1058 (for example).

"Dijkstra distantiated himself "

Hi. About:

>> To further clarify his research agenda, Dijkstra distantiated himself from dominant
>> traditions in logic, philosophy, and mathematics.

That's a great word, "distantiated" (a la "instantiated").

You just might be its inventor. Most of us less creative types would have written "distanced".

:-)

Todd S.
Houston, Texas, USA

distantiate

In dutch we use it more like:

"disassociate oneself from: "

then like

"set or keep (something) at a distance, especially mentally:"