As almost all of Dijkstra's writing, this piece here is a plea for teaching formal methods. It's nicely written I admit, but it is also unbelievably smug and disconnected from reality. Even in physics or mathematics, which are obviously much more mathematically tractable than computer science, people do not do significant new things by using only formal methods. In fact, the technical achievement Dijkstra is most known for, Dijkstra's algorithm, was not invented using formal methods, but like most discoveries ever it occurred in a flash of insight after a long period of thinking, as he said in an interview. No matter how much one loves rigour, the dream of formalizing all reasoning has turned out to be a pipe-dream, as evidenced for example by the failure of the Hilbert program, and people everywhere proceed about their business as usual.
Mathematics is not, after all, just the manipulation of a string of symbols, and neither is Computer Science, even if all computers do is exactly this, because we humans are complex beings, largely driven by emotions, not consciously aware of all the reasoning processes going on, that are often reasoning in "fuzzy" ways (and frequently with good effects), as opposed to being machines executing chains of logical inferences. In fact, people are born with very different internal worlds, some people are really good at symbol manipulation, algebra, and language, their daily thinking consists of "talking to themselves", while some people naturally think by imagining pictures and having various loose sensual impressions, among the latter for example the great mathematician Poincare. Was Poincare in need of someone to "really teach him mathematics"? Unfortunately I think Dijkstra assumed everyone is identical to him.
Before preaching this too much, look at the practical implementations of his ideas on this, for example have a look at him lecturing on a technical topic:
http://www.youtube.com/watch?v=qNCAFcAbSTg
or read "A discipline of programming". As nice as the EWD prose is, I honestly can't stand the man talking about anything technical for more than 5 minutes. The more concrete the EWDs get the worse they are.
For some perspective on how science really gets done, as opposed to people's romantic images of how it is done, I recommend "The Sleepwalkers" by Arthur Koestler, about the Copernican revolution, and "The psychology of mathematical invention" by Hadamard.
What he states is that computers are a "formal method applying machine" (a conclusion you seem to share), and that for competently using it, one must know formal methods. And, honestly, I can't imagine how one can disagree with that. (And that was the fate of EWD, he saw all the patently obvious problems of computing science that somehow everybody was ignoring, and communicated them, just to be called a crazy radical at first, and "duh, of course it's right, tell me something not obvious next time" later.)
He is proposing formal methods as a way of thinking about developing computer programs, this is clear from reading "A Discipline of Programming". You can not say "formal methods are a way not to think", because the theoretical existence of a sequence of transformations giving you the final program does not tell you how to find those transformations, so some thinking on the part of programmer is still needed. Of course you can come up with a program by a way of thinking completely uninformed by the formal specification, and then formalize it, but this is not what Dijkstra is speaking of in this article. What I am saying in the comment is that I do not believe many people benefit that much from a formal approach to program development, just like not that many new theorems in mathematics, outside of mathematical logic, were discovered using the tools of mathematical logic. Even the proofs themselves in mathematics aren't done in a completely formal way.
If you create a program in such a way that the properties you claim it has cannot be, even informally, proved. Then you have no reason to believe it works as advertised what-so-ever.
He did also propose a research program in to more formalised transformations and so on to help the programmer - which is a separate thing. But we all know about the difficulty of this and it's failure to materialise in any significant way (yet) for the average programmer.
The reason that that is, or was, a tantalising prospect is that when humans construct correct programs using informal proofs, they are using the same very simple abstractions over and over again. Therefore a system to automatically transform specifications to programs or whatever need not have all the troublesome properties of completeness and such like and may, in fact, be quite tractable. It's debatable whether anyone still think's that that's likely.
On the other hand, we teach a simple, clean, imperative programming language, with a skip and a multiple assignment as basic statements, with a block structure for local variables, the semicolon as operator for statement composition, a nice alternative construct, a nice repetition and, if so desired, a procedure call. To this we add a minimum of data types, say booleans, integers, characters and strings. The essential thing is that, for whatever we introduce, the corresponding semantics is defined by the proof rules that go with it.
This sounds exactly like a description of:
http://en.wikipedia.org/wiki/Predicate_transformer_semantics
And of the approach he uses in "The discipline of programming", so I think you are the one who is confused.
Ugh, that is unbelievably smug and disconnected from reality.
I could post tomes on why you are wrong. I will be kind and request you to respond to just this. :)
http://www.nytimes.com/library/cyber/week/1210math.html
Automated reasoners have been quite useful. You just have to stop being so smug and start looking.
Your complaining is like the physicists ("natural philosophers"?) at Newton's time complaining that natural philosophy (physics) does not need all that weird math and normal language is enough for physics.
You can't take this paper (or any other) as an end-all/be-all statement isolated in a vacuum. Maybe his smug tone portends that he might presume as much, but it's a mistake to take it as a one-size-fits all remark.
The thing he gets right is this:
Teaching students "Computer Science" as a new discipline by showing them how to reverse engineer existing examples is a mistake.
It's a mistake in the same sense that you don't teach math by giving students a number and asking them what the problem was. That's an absurd approach to math.
96.
Okay, now give me the equation.
That's the idea he's driving at. And in many ways he's right.
Does that mean that reverse engineering is a completely invalid approach to learning? No. For some disciplines, it is essential, and indeed, for certain aspects of electrical engineering, which ulimately melds with programming, one needs those sorts of strategies ready at hand.
But when it comes down to writing programs, he's cautioning that you should learn the task as a top-down approach, not by starting at the bottom, and then climbing up through someone else's ready-made tangle of spaghetti.
Does reverse engineering work for medicine and biology, or even chemistry? Well, what the hell kind of a choice did we have? Humanity had to bootstrap out of hunter/gatherer mode one way or another, but it doesn't mean we have to approach computer science the same way, and in fact, there's no rational reason to do so.
Read deeply enough into this message, and you'll unravel the mystery of why open source development is beneficial and generous, and proprietary closed source products really do represent a malign animosity toward the end user, by only providing the bald number as the result, and never teaching the man to fish. But hey, there's that old refrain: we all gotta eat right, so how do we make money when we're giving everything away and not rationing a portion for yourself?
Dijkstra comes from the era when computer scientists were a priesthood, moreso than tradesman. Computer science was esoteric, and so there was no fear of "teaching a slave to read" because there really weren't enough books to go around. Computers were high holy temples of time sharing cloistered atop the ivory tower. But in his message here, you'll gain insight into the fundamental truth, that when there are billions of cycles per second, acting on trillions of bytes at a time, there's no hope of brute force reverse engineering the resulting output of the system as a post mortem. Sometimes that's what we're stuck with, but it's not the ideal, and it's an impractical approach, not unlike picking up the pieces of an air disaster on a mountain top. Code needs to be well organized and properly conceived from the outset, and this is the desired approach, and a fundamental principle new students should have beaten into them, mercilessly.
In fact, one of the most important skills to learn for prospective computer programmers is rigorous design of experiments to confirm or deny a given thesis about some aspect of a given system. When you are dealing with a virtual machine on top of an operating system, communicating over a network through tcp/ip with another virtual machine, there are millions of lines of source code involved, not to mention potential hardware issues, how can anyone be expected to understand all of it? Even if some of this complexity is accidental, as soon as we get rid of it we will just build more sophisticated systems, so people will regardless have to know how to deal with systems that do not fit in ones head all at once and where you can't always just reason your way out.
I love computer science and teaching it is some of the most fun I've ever had. With a lot of practice, you can get across concepts such as computability and turing machines to the non-mathematically initiated within the duration of a party, and it's greatly satisfying. (yes I am a lot of fun to be around)
The rest of the EWD notes are highly recommended. (also it's weird to see an academic write in script). Side question: do any other HNers keep notes in written form? I still do it, using a fountain pen, and am often poked fun at by colleagues :(
[0]: http://academic.ianclarksmith.com/Coursera/DesignArtifacts/c... (Uniball .28 and mechanical pencil on blank 4x6 card)
By now I probably have thousands of these scattered throughout books (I use them as bookmarks while taking notes) or in boxes. They're not particularly well sorted except for being vaguely chronological. I have a decent stash of notebooks as well but haven't used them since it was a requirement for school except for a single pocket notebook that gets filled roughly once a year.
I've seen people struggle with tablets and laptops for note taking, but I find they are some way off the free-flowing UX of pen and paper.
Keep at it!
I used to mostly take notes with pens on sticky notes, but after a particularly tricky production debugging session I managed to cover most of my cubicle with about 60 hastily scribbled yellow sticky notes. I then proceeded to go on a trip for a week without cleaning up.
After returning I had to dispel a rumor that I had finally "snapped".
I think this is more of a designer concept but you can apply it to engineering as well.
https://news.ycombinator.com/item?id=43978 : A few comments
https://news.ycombinator.com/item?id=1666445 : Many comments
https://news.ycombinator.com/item?id=3553983 : Many comments
In the earlier threads there are two main voices: "Where can I learn more about this," and "It's useful to see the different perspective." Both say that there are many nuggets of wisdom to be mined, even when they don't agree. There are also a few who dissent and say it's irrelevant, impractical, and inapplicable.
Even in 3553983 where the top comment says it's largely irrelevant there is a useful dialogue discussing the ideas, and how they can be made to work, or at least how we can learn from them in today's context.
In contrast, in this thread so far we've mostly had comments about the hand-writing, and complete dismissal of the ideas. So far there's very little attempt to say: "OK, times have changed, but can we learn something from this?"
So I ask - Can we? Are there nuggets to be mined? Or are you convinced that you really do know better, and have nothing to learn from it.
I'm still learning.
========
For reference, other submissions, mostly without comments:
https://news.ycombinator.com/item?id=6701607
https://news.ycombinator.com/item?id=2122826
https://news.ycombinator.com/item?id=2090256
What we write today is WoW and stuff we don't need formalism to prove they don't crash - because, you know, who cares about that?
Dijkstra comes from a time were you could reuse a piece of software and build upon it because you could understand it. Today nobody does it because the software is "disposable". Who cares about proving a piece of future garbage?
People learn differently and formalism in one approach to teaching it. It has it's purposes but complex systems require more than one way of representing it. Formalism shouldn't be the only way to represent and teach the concepts of computation and CS.
You are right in saying that formalism is required to trust the result; however, I would argue that it isn't the only way. Looking at something from a strictly mathematical approach would ignore some of the more black arts component of CS and Software development. You should be viewing a system from various angles to help convince you of it's reliability.
I think these two talks might help explain things.
http://worrydream.com/MediaForThinkingTheUnthinkable/ http://www.confreaks.com/videos/282-lsrc2010-real-software-e...
"And with the sixth example I have reached imperceptibly but unavoidably,
the most hairy part of this talk: Educational consequences."
"The effort of using machines to mimic the human mind has always struck me as rather silly. I would rather use them to mimic something better."
Jesus, could he be any more smug?
Funny that I think that statement is extremely humble.
The manner in which Dijkstra writes about this is very off-putting - it sounds arrogant and one-sided, dismissive. In fact he comes across as ignorant, which of course, he is, in this area.
Worryingly, I see a lot of similar writing in CS blogs. Often authors present as fact their opinions on a topic that they are not knowledgeable about.
When I read something like that, I look for the balance in their argument. If they say "well, what are the good sides to teaching by analogy? When does it work best? What is the evidence that teaching basic arithmetic is done well?" then I begin to take them seriously.
[edit: typo]
I loved it and emailed Prof. Dijkstra during the brief time that he finally had email (I got a graduate degree from his department and attended some of his classes). I asked him for permission to one day create a font from his handwriting, not really expecting a response.
However, he did eventually reply, granting me the permission to do so.
I commissioned the font and it worked nice. It was distributed briefly and it may still be out there (I see one or two are found out there).
My original copy may be in old backups. One day I will find it and update it!
Edit: found the email reply! He retired in 11/1999 and passed away in 8/2002
Austin, Tuesday 11 April 2000
Dear Dr. Puchol,
If a competent designer can use my handwriting as a source of
inspiration, that is fine with me. Thank you for asking my permission,
which is granted with pleasure.
With my greetings and best wishes,
yours ever, Edsger W.DijkstraHowever I think this needs to be coupled with an introduction to the concrete at a younger age. In mathematics we teach arithmetic to young children then step up the ladder of abstraction to high school algebra, simple proofs and linear algebra before eventually exposing them to abstract algebra (ie group theory etc). Teaching abstract algebra first would make theoretical sense but the mind tends to need to know at least one example of something before it accepts the abstraction.
I imagine a playful introduction to programing for young children coupled with a strong course in formalism for young adults could produce some great programers. Though, as with the proof based math series I took, I'm sure there would also be loads of freshman drop outs/transfers to more applied courses.
I also agree with others that insight rarely comes from pure formalism. The point of learning these things is to expand the way your mind works allowing you to think about abstract objects and allowing you to verify insight when it does come.
For me Charlie Parker sums up the necessity of a formal education even if it is not explicitly used in practice:
"Master your instrument, master the music & then forget all that & just play."
How very true across so many aspects of life!
Science doesn't happen through formalism. People learn the body of material that's been proven, then they get new intuitions, then afterwards they try to formally prove their insight. This isn't entirely inconsistent with EDW either. A lot of his point is that programmers need to know how to think symbolically, and if you truly prove the correctness of things, you can build the base of knowledge on top of it. If not, you're frequently wondering why things don't work.
Software engineering, of course, presents itself as another worthy cause, but that is eyewash: if you carefully read its literature and analyse what its devotees actually do, you will discover that software engineering has accepted as its charter "How to program if you cannot".
My point today is that, if we wish to count lines of code,
we should not regard them as "lines produced" but as "lines
spent"It is the difference between "change" and change, "thinking" and thinking.