On the other, I was present at an IFIP talk he gave in Toronto in 1976 where he announced that personal computing would go nowhere, because the average person cannot program.
> "I don't know how many of you have ever met Dijkstra, but you probably know that arrogance in computer science is measured in nano-Dijkstras." - Alan Kay
With the followup post from Alan Kay himself.
But still, let's say there is a problem someone wants to solve, and it really doesn't take much programming to solve it? How do regular people that don't have access to a programmer use a computer to handle a novel problem?
To give an example -- There is a table game that is popular at Cracker Barrel restaurants that consists of a triangle shape with 15 holes, and 14 golf tees. The object is to jump over pegs and remove them, and go till no more moves are available. The goal is to get down to 1 peg remaining. Now how would you use a computer to solve that without writing a program? (This was back in my college days, however I recall doing a brute force program that tried all combinations, and spit out the winning ones -- turns out there was something like 15,000 winning strategies).
Edit -- a quick search shows that this has become a popular computer programming challenge, so there does exist choices that people can download, but there are other similar variations that someone may want to solve.
Edit2 -- apparently the generalized version of this concept is called Peg Solitaire https://en.wikipedia.org/wiki/Peg_solitaire
EWD was right in the sense of his definition of "Program" i.e. as a mathematical object. What he did not quite foresee is that it takes only a few intelligent folks to invent/design/implement the entire infrastructure so that the general "mass of programmers" can use those to certain profit without much mathematical background. This was how the "Industrial Age" played out, we use a lot of machines everyday without having an inkling of how they work. I think Dijkstra failed to realize that this was as true of "Software" as of material objects. In his defense, the "Software Industry" was still being invented at that time and hence nobody could predict how things would turn out in the future.
But his fundamental thesis that a "Program" should be treated as a mathematical object and proved using rigorous logic is still true and by that definition a lot of us fail the test. This is quite independent of the fact that the society at large has accepted a watered down definition of a "Program" with all its shortcomings and failures.
How is that even remotely true? How are you going to formally model a browser, or a word processor, or your mail client, or a 3D game, let alone prove it correct against that specification?
If we actually followed that requirement, computers would be almost useless today, except for a few tiny niches where millions of dollars in development costs for even relatively small programs would be justified. Keep in mind that your development tools would be meager to non-existent as well, since they'd also have to satisfy that overly strict requirement.
Don't forget there's a difference between a formal (user) specification and a functional specification.
A functional specification says that when you select "Edit -> Cut" the user can expect certain things to happen. A formal specification defines how the symbolic entities involved in implementing the operation should operate.
This isn't too hard for "Edit -> Cut", but it's not tractable at all for "Translate this poetry into another language without mistakes or ambiguities."
So in fact he's just as guilty of resorting to metaphor as anyone else in computing. Only in this case the metaphor is the algorithmic perfection and consistency of a mathematical proof.
This is fine in the classroom and in certain applications where formal methods can help, but not so much in the average developer room.
It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets.
But I expect he'd have dismissed that idea as too dangerously novel.
Not quite. Computers only deal with Symbolic Logic via Formal Systems. The mapping of those to a Domain of Discourse is the job of the Programmer.
Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem.
You can also find some relevant discussion (including my posts) at https://news.ycombinator.com/item?id=24942671
The point is that by using a top-down and step-wise refinement methodology one can show "correctness" at whatever level of granularity is acceptable.
PS: "Excel" can be thought of as a program generator which specifies a metalanguage (i.e. a "grammar") for a set of DSLs (i.e. Spreadsheet formulas). A little Googling brought up "ViTSL/Gencel"(https://web.engr.oregonstate.edu/~erwig/Gencel/) and "Classheets"(http://www.jot.fm/issues/issue_2007_10/paper19/index.html) showing approaches to specifying "correct" Spreadsheets.
Software engineering != developing algorithms. And unfortunately programming can mean both things.