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.
> But his fundamental thesis that a "Program" should be treated as a mathematical object and proved using rigorous logic is still true
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.
Quite. It's the silliest of silly ideas - not just practically, but conceptually, because real problems don't have hard algorithmic edges. Which is why they're so hard.
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.
>It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets.
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.
Here is Dijkstra himself answering the charge via EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition".
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.
What would a coarse-granular specification for Excel look like? How would you prove correctness against such a spec? Examples, please. In these discussions, I only ever see vague statements and handwaving by formal verification proponents — which is kind of ironic, when you think about it...
I believe you are being facetious here. This is a forum for stimulating discussions and exchange of ideas. The fact that you only "see vague statements and handwaving" is more a reflection of one's knowledge bank (or lack thereof) than any shortcoming of the subject or its proponents. By definition this is a complicated and difficult subject and when a computer science pioneer and great like Edsger Dijkstra says something, you pay attention and think about it :-)
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.