[throwanem]

One would as sensibly dismiss the concept of an assembly line as "how to build a car if you cannot."

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.

[_dwt]

The formal methods people may yet have the last laugh. I did not have Lean becoming a hyped programming language / proof assistant on my bingo card for 2025-26 and yet here we are, because these tools help us close the validation loop for LLM agents. That is not dead which can eternal lie...

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.

[throwanem]

Certainly, and it's at that economic argument that I strive to get, I think.

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.

[1] http://sunnyday.mit.edu/papers/therac.pdf

[ThrowawayR2]

There is no liability or penalty for software defects and therefore no incentive for program correctness. Arguably, Dijkstra didn't fail; society has foolishly decided not to hold developers accountable for their bad code.

[throwanem]

Arguably? Okay, so argue it.

[bigfishrunning]

I think the real tragedy here is that we can spend *all* of our time trying to improve the quality of our output, but it simply doesn't matter, because as long as the button is where the boss wants it to be and is the right color, all is right with the world.

Literally nothing else matters, and we (or at least I) have wasted a ton of time getting good at writing software.

[throwanem]

As long as it continues to matter what the button actually does, I can't consider our effort to have been entirely wasted. We only have the misfortune to live in stupid and dangerous times, but good heavens, we're hardly the first in that, and hardly starved for examples from whom to learn.

[zephen]

> One would as sensibly dismiss the concept of an assembly line as "how to build a car if you cannot."

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.