And so these are now no longer problems? Or do they remain thorny matters in practice, precisely because the versions that Djikstra solved are narrowly defined and without awkward external requirements?

Good software engineering largely rests on taking whatever "awkward external requirements" you're dealing with and decomposing them by concerns until you have a set of "narrowly defined" problems that you can effectively reason about, formally or informally. Dijkstra was a master of that kind of decomposition and that's how he got the interesting "theoretical" problems he solved: they came up in the course of breaking down practical problems!

The point then is that with the concerns having been adequately separated, rigorous, disciplined, and mathematical reasoning is a better approach to thorny "real-world" problems than spitballing and hoping it works.

> Good software engineering largely rests on taking whatever "awkward external requirements" you're dealing with and decomposing them by concerns until you have a set of "narrowly defined" problems that you can effectively reason about, formally or informally. Dijkstra was a master of that kind of decomposition and that's how he got the interesting "theoretical" problems he solved: they came up in the course of breaking down practical problems!

Every good software engineer breaks down the problems they have to solve, and usually you find that they're, say, 20% interesting theoretical problem and 80% messy practical drudgery. Unfortunately most of us don't have the luxury of choosing to only solve the nice 20%.

> The point then is that with the concerns having been adequately separated, rigorous, disciplined, and mathematical reasoning is a better approach to thorny "real-world" problems than spitballing and hoping it works.

What's the evidence for this? Because if Djikstra published a paper "solving" the problem, but the problem was not actually solved in the real world, that to me suggests that his approach is decidedly ineffective.

> What's the evidence for this? Because if Djikstra published a paper "solving" the problem, but the problem was not actually solved in the real world, that to me suggests that his approach is decidedly ineffective.

Another possibility is that the field is dominated by coders who are mathematically illiterate and unwilling to remedy that deficiency while hiding behind rhetorical hand waving about the “real world.” You yourself appear to stand as evidence for that explanation.

Fortunately we are seeing some real progress in the field. For example tools like TLA+ are slowly but surely getting wider and wider usage. Lamport is very much in the same school of thought as Dijkstra by the way. Even TDD represents a major step toward a more disciplined approach to programming.

> Another possibility is that the field is dominated by coders who are mathematically illiterate and unwilling to remedy that deficiency while hiding behind rhetorical hand waving about the “real world.” You yourself appear to stand as evidence for that explanation.

I'll take the gratuitous personal attack as a sign that you have no real argument. "coders who are mathematically illiterate" doesn't explain anything. Even in the research mathematics community it's acknowledged that if you haven't communicated your proof to others then you haven't proved the theorem (see all the fuss around the ABC conjecture).

I'm all for mathematical rigour in programming (and, not that it matters, I'm as experienced/qualified as a non-research mathematician can get). But judging how effective something is by how rigorous it is is putting the cart before the horse.

> Even TDD represents a major step toward a more disciplined approach to programming.

A step that Dijkstra would have abhorred; he used variations of "Program testing can be used to show the presence of bugs, but never to show their absence!" in at least a dozen different EWD notes.

Yes, Dijkstra invented the semaphore, but that "solved" synchronization about to the extent that John McCarthy inventing the linked list "solved" data structures (or FAANG hiring, for that matter).