3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I you want a soft and enjoyable introduction to the use of formal logics in algorithm design (not just proving but effective design), I warmly recommend you "A Method of Programming", by Dijkstra, Edsger W., Feijen and W. H. J., Sterringa, Joke. $\endgroup$ – Yves Daoust Sep 26 '15 at 13:54
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Hmm .. I wonder then why he speaks of the necessity of formal methods as though it were already a foregone conclusion. $\endgroup$ – Eli Rose -- REINSTATE MONICA Sep 27 '15 at 15:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.