What this talk essentially proposes is to scrap the teaching of an approach to program development that has produced pretty much EVERY SINGLE piece of practical software used in the history of computing, in favor of an approach that had not produced, to my knowledge, a single nontrivial piece of software by 1988, when the talk was given, and has not produced, to my knowledge, a single piece of software in the 20+ years since.
In a separate thread, I have posted De Millo, Lipton, and Perlis' 1979 argument against formal methods: http://fresh.homeunix.net/~luke/misc/p271-de_millo.pdf and 30+ years after that article, and 20+ years after Dijkstra's talk, I don't see how there can be an argument as to which of the two views has prevailed in practice.
I would welcome hearing Dijkstra's view argued, but I would find such an argument much more compelling if it included citations of actual, working programs (as opposed to isolated algorithms) that were developed with end-to-end formal methods. It would be even more compelling if the argument included published proofs of such programs and/or the author's personal experience developing them.
Had this done to me, in 1981 or so at the University of MD. They decided to teach some kind of "theory of proving programs correct" to a bunch of CS-101 types who were just learning Pascal, too. I guess the hope was that we'd get a healthy dose of mathematical proofiness and write better programs.
One of our first lectures: "Taking this loop, we prove by induction that it computes the sum of the first ten integers. Here are a bunch of logic formulas (lots of scribbles on the overhead). Here's a bunch of notation, it's got CONJUNCTION and DISJUNCTION and COMPOSITION and so forth. By inference [and some hand-waving] this five line program computes a sum, yes?"
Class: "Huh?" Not even panic, just a collective, bug-eyed "<I>What the fuck?</I>?"
The approach failed miserably; what it /did/ successfully teach was cynicism; most of the students were really upset at the obvious nonsense. [I was the only one of about 250 students to complete all the project work . . . and I cheated by writing the project in LISP, and writing a LISP interpreter in Pascal]
People certainly have written real software using formal methods: http://compcert.inria.fr/ is a good example.
Of course this does not constitute an argument that programming must be taught as a formal discipline, but it does indicate that formal methods can be useful in some circumstances.
Interestingly, http://compcert.inria.fr/release/Changelog mentions various "bug fixes" in almost every release, and the mentions of "successful tests" are not quite canonical either, but it certainly looks like a successful, nontrivial program.
Yes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts).
It does make a nice poster child for formal methods though.
I mostly agree with him that the paper is poorly argued (I have no love for formal verification). However he ignores the most salient point that it makes: that the effort of verification must be applied everytime a programmer makes a change to a codebase.
Entirely appropriate, assuming the post is interesting, which this one is. Pity it got lost in the shuffle.
Advocates of formal verification of software remind me of the old joke, usually about a Frenchman but sometimes about an Irishman, who says in some policy debate: "I can see that it works in practice, but will it work in theory?"
Dijkstra is one of my favorite writers on programming, but I can't resist pointing out that he was on the wrong side of "how to program if you cannot." We have a huge, thriving, valuable, and quite reliable information infrastructure built out of incorrect programs. Dijkstra believed in correct programs and believed that software engineering would not succeed without them. He believed it was counterproductive to teach people to program and employ them as programmers if they could not write correct programs. He believed that the future of computing would be defined by the struggle to write correct programs, and that even if we managed to get by with incorrect programs, the cost would be much greater than if we had achieved the same results via correct programs.
Wow! Can you imagine where we would be if we only had code written by people who had completed rigorous training in mathematics and formal methods? Can you imagine a world where the middle ground between mathematics and the analog world was completely bare? No Excel spreadsheets made by accountants, no customized HTML or CSS, no wiki markup even, because you can't trust amateurs to do programming! It's hard to wrap my head around the idea that The Print Shop for the Apple II should never have existed, because the small minority of people suited for Dijkstra's rigorous training in mathematical programming would surely have been engaged on far more important projects.
Hmm, the essay is dated 1988. I wonder if he still believed that a small class of elite programmers armed with formal methods would have created all of the wonderful programs I used at school around that time -- Print Shop, Where in the World is Carmen Sandiego?, Math Blaster, and on and on -- did he believe his mathematician/programmers would have created all those programs and even more? Or was he simply out of touch? Ah, but how wonderfully and brilliantly out of touch.
He is also wrong about software aging and needing maintenance, as well, but there is an important lesson to learn from what he said. As usual, he is right about the mistake in language even though he is wrong about the phenomenon it refers to: programs are routinely transplanted from one context to another, because it is expensive or inconvenient to maintain their original context. Aging and maintenance are a poor analogy. Using poor language to address something is, in practice, less wrong than simply ignoring it, but we would be better off if we heeded Dijkstra's advice not to lean on bad analogies for novel situations.
Dijkstra was right though. We have credit card thefts, SCADA systems run amuck (Iran's nuclear centrifuges for example) and serious risk to life and limb as a result.
The thing is, we can't measure how much better off society would have been had we baked those rigorous methods into the base of our tools. Or the benefit in increased velocity if we didn't have to come back and fix stupid defects later.
Further, with TDD, BDD, unit tests, etc we're slowly moving towards the world Dijkstra argued for in the first place. Dijkstra could see the Forrest while industry was bedazzled by the trees.
If you want proof, you will always agree with Dijkstra ;-) Unfortunately, I can't summon an alternative universe where Dijkstra got his way. However, I can say that Dijkstra is rolling over in his grave if he heard you compare testing to his approach. To him, empirical approaches were appropriate for the physical world, where items vary, materials deteriorate, and operating conditions are unpredictable. In the digital world, where systems are vastly more complex but made out of ideal, eternal elements, the proper tool is not empiricism, but mathematics. That is Dijkstra's message: mathematics is the right tool for programming, and we are making a costly error by applying empirical engineering methods instead.
Testing is just another messy empirical approach to a mathematical system. The master would be appalled.
I would think that unit tests have nothing to do with Dijsktra's notion of verification. I even seem to recall he had a horror of software testing. If you can prove something, why test it?
I recently read the free Kindle chapter of David Gries' book The Science of Programming, recommended at a previous discussion of this essay:
http://news.ycombinator.com/item?id=1667081
My impression of his thesis so far: unit tests are great, but the challenge is figuring out exactly what unit tests you need to write. Formal methods give you a way of doing that.
It has been written, I think by Dijkstra himself, that he has a (mid 20th century) European perspective on computing: that computers are prohibitively expensive and so we must go as far as we can with math before hitting he hardware. This is contrasted to the American view that hardware is free. Obviously the American view has won out over time.
I've never heard of this difference in perspective between Europa and the US. Do you have anything to support that?
But anyway, this was written in 1988. As someone who was already a programmer at the time, I can assure computers weren't viewed as "prohibitively expensive" in Europe.
Maybe this difference existed ten years earlier, but not in '88.
I thought it had more to do with European CS departments often being considered part of math while American CS departments were often considered part of EE. That would account for some difference in the habit of buying hardware in the beginning (say 60s and 70s): EE already had to buy a lot of that while the math department did not, so it was a new thing for a department that generally did not have high capital expenses.
But I don't think the ability to buy hardware is as relevant as the different mindset between mathematicians, who focus on more abstract problems, and engineers, who focus on more concrete problems, especially today when hardware is cheap. Being an American-trained computer science and spending some time working in Europe, it definitely felt like more emphasis was placed on formalism vs. engineering.
I think it may also be related to a historical experimental/mathematical difference. Edison (US) admired Lord Kelvin (UK), who believed in constructing physical models of theories. He thought you had to be able to see it. Whereas Laplace and other French (EU) mathematicians favoured a symbolic mathematical approach.
Lord Kelvin had a minor win, in that he refuted one of Laplace's mathematical constructs with a model. Edison also had some wins. But of course, Einstein had the biggest win of all, using a symbolic approach (he began with clear visualizations which he later found mathematics for. There were other factors, but once he switched to a purely mathematical approach, he had no more breakthroughs...)
I personally wonder if this US/EU distinction is somehow be related to having all the land already being owned vs. land available.
PS: I'm taking this from biographies of Edison and Einstein, so please correct me if I'm wrong or omitted something relevant.
Implicit in your comment is the claim that the current state of software engineering is good. Just because a lot of helpful/entertaining/profitable software has been written doesn't necessarily mean the industry is in a good place. Especially outside the startup world, I suspect a lot of money and time is wasted because software projects run over budget or over time.
No harm, no foul, it's a good read, I'm merely pointing out previous discussions so people can see what the HN commentators thought on earlier submissions.
And for reference, the URL dup-detector works mostly on exact matches, and even then, only on stuff in cache. Probably.
> [Anthropomorphism] is paralyzing in the sense that, because persons exist and act in time, its adoption effectively prevents a departure from operational semantics and thus forces people to think about programs in terms of computational behaviours, based on an underlying computational model. This is bad, because operational reasoning is a tremendous waste of mental effort.
I see the effects of this every day at work. And the resulting programs are indeed much complicated by needless uses of procedural style.
It appears most programmers are completely oblivious to the fact that most computation is completely timeless. It's pure functions. It's static. Just like good old fashioned Math™. Nevertheless, they go on introducing time, change, and all the complexities and errors that goes with them, just because nobody taught them to think any better.
It is quite infuriating that I am sometimes forced to follow that trend, sometimes because otherwise my colleagues wouldn't understand my code, but more often because the APIs they wrote are based on mutation when there was no need, or their functions aren't total even though they could have been.
Wow. I have not been exposed to this before, and I was just buzzing by for a quick scan of Hacker News. I have stuff I'm supposed to be doing, and I had NO idea I was going to get sucked in to such an enlightening, insightful read!
The most insightful point, to me, was this -> A "program" is a formal system for abstract symbol manipulation, and therefore, the most effective way to produce/improve/"maintain" programs is to reason about the program itself (as opposed to, for example, testing every conceivable input and output).
My summary leaves much to be desired, but maybe it gives you a TLDR idea of what Dykstra is saying. If you're a programmer, read it.
What introductory programming course is he talking about?
(... when he says, "since the early 80's, such an introductory programming course has successfully been given to hundreds of college freshmen each year" ??)
Guessing: given where he worked, that must be either Eindhoven or UTexas. Given the 'hundreds of college freshmen each year', I find it hard to believe it could be Eindhoven.
What a great essay. There are so many points and places to branch off of and explore. I'll limit myself to a question about the following quoted part, though. It does look like it was slightly explored in other discussions so maybe it's not that interesting, oh well.
"Like all digitally encoded information, it has unavoidably the uncomfortable property that the smallest possible perturbations —i.e. changes of a single bit— can have the most drastic consequences."
Is this really a unique fact about digital vs. analog systems? I'm not inclined to think so. He gives the example of pressing slightly harder on a pencil to get a slightly thicker line. Another possibility is that by pressing slightly harder, you cross the threshold of the paper's strength and wind up with an ugly hole. In the digital world, if I change the low-order bit of a single number in a single calculation, the result will be only slightly inaccurate. We can still get to the moon on inaccurate digital calculations. If I change the high-order bit it will be more inaccurate, and if I continue using the results then errors propagate. Similarly if I keep trying to draw over the hole in the paper I'll just wind up with a bigger hole. To put it shortly, initial conditions matter. Another way to put it, some small changes may indeed have large effects, some small changes may indeed have small effects, but you need to know what changed and in what environment the system is in in order to have any idea what to predict. Another way: any analog/continuous thing can be discretized, so is the problem with the discrete property itself so that only continuous systems that have been discretized will exhibit the problem, or is it fundamental to everything?
It seems to me that humans by default think that small changes can only have small consequences, whether those changes are to an analog or digital system. Small->Big is surprising when it happens. I'm sure there are lots of just-so evolutionary psych stories you could come up with to suggest how our brains got this way too. Imagining in great detail the huge effects made possible by such a small action as Stalin counter-factually being run over as a kid takes a lot of brain power that could be spent gathering food, consider how it might feel to have to imagine grand series of causes, effects, counter-factuals, and so on for 8 hours a day. (Or get back to doing it if you're a programmer at work.)
So I think Dijkstra is really getting at the fact that for the first time ever humans (programmers) have to be face-to-face with these hugely complicated systems, and they have to come to terms with the fact that tiny changes can and will cause big effects. In this sense, the second radical novelty of computing is just a special case of the first: dealing with the dynamics of fine-grained discrete systems like that of a digital computer is a big intellectual challenge for us when we're used to reasoning over Fuzzy or just large intervals.
After the section I quoted, Dijkstra points out that even with error correction the picture isn't changed. But I think error correction does significantly alleviate the problem--human bodies are also incredibly complicated but they're also robust and they have many error-correction features like an immune system. Computer programs on the other hand are extremely fragile. Nevertheless a single stupidly tiny virus with a simple DNA signature that is introduced to a human can cause that human to later die! In one of the other discussions someone mentioned that a tiny DNA change results in a lack of an iris. For all of our body's resistances to mitigate changes, we still can't escape the seemingly fundamental problem that small changes can cause big effects.
Edit: On the example Dijkstra gives later on with the board and the dominoes, I knew I had seen that problem before. I saw it first here where it has pictures: http://lesswrong.com/lw/rb/possibility_and_couldness/
> Another possibility is that by pressing slightly harder, you cross the threshold of the paper's strength and wind up with an ugly hole.
As you press harder, the paper gets more and more compressed. You can't go directly from 1mm thickness to hole.
> In the digital world, if I change the low-order bit of a single number in a single calculation, the result will be only slightly inaccurate.
If your single number represents a boolean variable, then it will be completely innacurate.
And the behaviour of a program can be completely different depending on the value of that single variable: exit instead of resuming; change the value of $bank_account_amount instead of waiting for the lock; dereference an invalid pointer, etc. Note that these aren't especially crafted examples. They could happen with existing programs, and actually do every day.
Of course you could come up with real examples of small changes in an analog system resulting in big changes, but Dijkstra's point is not that such things do not exist, only that it is not the rule in analog systems we're used to dealing with.
In a separate thread, I have posted De Millo, Lipton, and Perlis' 1979 argument against formal methods: http://fresh.homeunix.net/~luke/misc/p271-de_millo.pdf and 30+ years after that article, and 20+ years after Dijkstra's talk, I don't see how there can be an argument as to which of the two views has prevailed in practice.
I would welcome hearing Dijkstra's view argued, but I would find such an argument much more compelling if it included citations of actual, working programs (as opposed to isolated algorithms) that were developed with end-to-end formal methods. It would be even more compelling if the argument included published proofs of such programs and/or the author's personal experience developing them.