World's most popular travel blog for travel bloggers.

What does Djikstra mean by "formal techniques" in this essay?

, , No Comments
Problem Detail: 

In this essay (and others) by Djikstra, he refers to "formal techniques" a number of times.

... for the computing scientist, formal techniques would play a much more important rôle than they had done so far for the mathematician.

... The practical reason was that formal techniques are indispensable for dealing in a sufficiently trustworthy manner with the type of complexities a program designer has to control.

In our history, the computing scientist seems to be the first to be asked to apply formal logic on a grandiose scale and to make formal techniques an integral part of his daily reasoning; in a way, circumstances have forced him to become more mathematical than the Pope is Roman Catholic.

... what else can you expect in a world that has never seriously tried to apply formal techniques on a sizeable scale with elegant effectiveness?

I have only a vague idea of what he means by this term (which I'm sure has to do with the context he was writing in in 1985).

Does he mean something like "formal methods" -- proving mathematically that a program you've written is correct? If so, his assertions don't seem very accurate -- we're not doing that on a "sizable scale."

From other essays, I have the idea that perhaps he means "programming in a language with a specified syntax." To my understanding, this would make the third quote make more sense -- his argument is that mathematicians have no syntax their formulas must follow -- but I don't know why this would be called a "technique" or why it would be called "indispensable", as though it's some new technological advance for writing programs. How would programs be written, if not in terms of some strict syntax?

So I'm not sure I get what he's saying.

Asked By : Eli Rose
Answered By : Yuval Filmus

It seems quite clear that Dijkstra did mean what is known today as formal methods. He also had the idea that calculations should replace mathematical proof in prose, which you can find in some of the EWDs. It seems that so far his dream hasn't been realized, and while formal methods are used in some extreme circumstances, the average programmer has no use for them.

Best Answer from StackOverflow

Question Source :

3200 people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback