Dijkstra was a mathematician. It is a necessary discipline. If it alone were sufficient, then the "program correctness" fans would have simply and inarguably outdone everyone else forty years ago at the peak of their efforts, instead of having resorted to eloquently whiny, but still whiny, thinkpieces (such as the 1988 example [1] quoted here above) about how and why they would like history to understand them as having failed.
[1] https://www.cs.utexas.edu/~EWD/ewd10xx/EWD1036.PDF [2]
[2] I will freely grant that the man both wrote and lettered with rare beauty, which shames me even in this photocopier-burned example when I compare it to the cheerful but largely unrefined loops and scrawls of my own daily hand.
But yes, I think the best rebuttal to Dijkstra-style griping is Perlis' "one can't proceed from the informal to the formal by formal means". That said I also believe kind of like Chesterton's quote about Christianity, they've also mostly not been tried and found wanting but rather found hard and left untried. By myself included, although I do enjoy a spot of the old dependent types (or at least their approximations). There's an economic argument lurking there about how robust most software really needs to be.
Every so often an article makes the rounds on the correctness and verification methods used for Space Shuttle avionics software and applications of similar import, or if not that then Nancy Leveson's comprehensive 1995 review of the Therac-25 accidents. [1]
Most software doesn't need to be nearly so robust, but Dijkstra constructs his argument as though all did, hinging the inversion on the obvious and frankly shocking cheat across the gap between his pages 14 and 15, ie, that paragraph beginning "But before a computer is ready to perform..." Here he casually, and without direct acknowledgement much less justification, assumes as rhetorically axiomatic that a program, not the machine that executes it, is the original artifact of computing, of which any reification merely constitutes less than perfect instantiation, which he is then free to criticize on the wholly theoretical grounds of mathematical beauty; that is, on the grounds he prefers to inhabit in all cases, whether to do so in any given example makes any sense or not.
If that's his preferred ground, fair enough; after all, he was a mathematician. But his hypocrisy in concealing the insistence by means of subtle rhetoric - mere pages after inveighing against "medieval thinking" by way of an example, his "reasoning by analogy," faulting specifically that argument made by way of specious rhetoric! - casts suspicion on all that both precedes and follows. From a layperson, I could regard it as honest error, but I have known and loved academic mathematicians, and I really can't conceive of any of them leaving intact so consequential a mistake.
Perhaps Dijkstra was different, or merely becoming old, but for someone so heavily invested in pushing a paradigm of programming with mathematical rigor at its core, it seems a remarkable flaw in what should be a crucial argument (especially in advance of a solution for the halting problem). I regret that flaw, because he isn't all wrong about what an engineering paradigm can do to the agency and optionality of programmers especially in industry - not that his one extremely privileged position therein, parallel with Feynman's time at Thinking Machines, would much acquaint him with our desiderata or our constraints - and I would like to find that point made in better company than he was able to give it.
But then, his conception never offered much in preference, did it? The labor of mathematicians is scarce and expensive: what good is a proof assistant to anyone who can't understand its output, much less give it input? And Dijkstra himself, not less strange a bird than any other mathematician, famously did all he could to avoid actually using the machines on whose correct use he here wrote. (Hence his hand, which I complimented so highly before. I also use a fountain pen, but as I said, not so beautifully - and I'm glad I know how to use a keyboard well, instead.)
There would not be more programmers or more software in a world run on such principles, I think, than in this one - on the contrary, less by far. Maybe that would be preferable, but mostly not for the reasons Dijkstra claimed.
Literally nothing else matters, and we (or at least I) have wasted a ton of time getting good at writing software.
I agree, but I'm not sure this says what you think it does.
The people on the car assembly line may know nothing of engineering, and the assembly line has theoretically been set up where that is OK.
The people on the software assembly line may also (and arguably often do) know nothing of engineering, but it's not clear that it is possible to set up the assembly line in such a way so as to make this OK.
Arguably, the use of LLMs will at least have some utility in helping us to figure this out, because a lot of LLMs are now being used on the assembly line.