Whenever this comes up I feel compelled to say that Dijkstra has a huge blind spot with this, that perhaps is more obvious with decades of hindsight. He advocates formal proof for a functional specification of a program to be part and parcel of writing it, and note that what he refers to by formal proof is ambiguous.

If he means the informal proofs mathematicians write and publish all day long, these actually include a lot of handwaving, metaphors, generalizations, and leaps of logic that the reader is presumed to be expert enough to fill-in-the-blanks. So for example, Wiles had a non-trivial bug in his proof of Fermat's last theorem that was thankfully non-fatal and fixable.

On the other hand, if Dijkstra was referring to formal proof, then without a proof assistant one still easily makes mistakes in it, and even with a proof assistant the task is so immensely tedious even now that even mathematicians don't do it, so why would programmers of non-safety-critical apps?[1] And another blind spot is that no formal proof will help you if your specification is wrong, and only give you false confidence: you can't navigate the world without errors if the only geometry you know is Euclidean.

[1]: of course, note that many people are trying to develop good enough proof assistants that mathematicians would feel add more value than remove via tedium. And also note that formal methods are being employed when the stakes are high enough; e.g. formal verification is performed on processor circuits.

One of my Uni professors was working on Proof-carrying code *(https://en.wikipedia.org/wiki/Proof-carrying_code). I got a cursory involvement. Although I agree with you, the fact that there is a way forward and is entirely based in mathematics (on the formal side) makes me also agreeable with OP. I don't see a contradiction. If you talk about the more informal side- the way something is used does not necessarily define its nature.

Indeed, I don't disagree with OP. I just felt compelled to point major problems with Dijkstra's argument, because it's somewhat generally known yet its very real shortcomings aren't as widely known.

The general response seems to be that "yeah, ideally we should be more mathematically rigorous with programs if we have time and mathematical expertise", but few have sufficient exposure to formal methods to understand that it's far from the panacea the memo makes it out to be and there are more reasons not to do it than just time and expertise.

There is a way forward, but it is tedious as all hell. I love formal methods. I spent years in grad school working in it. But the truth is that formal reasoning struggles to scale to interesting programs, especially if you have to consider open programs, and is utterly incoherent for most software engineers. You can compare something like symbolic execution, which seems amazingly elegant and powerful, with coverage guided fuzzing, which is hacky and random. Coverage guided fuzzing eats symbolic execution for lunch.

There's a lot more in that paper than an argument for formal proofs. In fact, formal proofs are more of an incidental idea than the main point of Dijkstra's argument.

For example, he suggests that we need to understand computer science as a "radical novelty" and stop applying inapt analogies that come from thinking about this like a gradual evolution of mechanical things.

Inapt mechanical metaphors include software "tools" and "workbenches" that require "maintenance". Getting stuck with bad industrial analogies is "medieval thinking" that prevents real understanding.

Yes, he advocates that we need to view it as a "radical novelty" and critiques existing methods, but the only better method he puts forth is with formal proofs; it's not incidental, it's the reason for calling existing methods backward and insufficient for managing programs.

> it gives us a clear indication where to locate computing science on the world map of intellectual disciplines: in the direction of formal mathematics and applied logic, but ultimately far beyond where those are now, for computing science is interested in effective use of formal methods and on a much, much larger scale than we have witnessed so far.

I'm not too interested in arguing point-by-point the other arguments for viewing them as a "radical novelty", but even mathematics deal in methods that require maintenance (e.g. calculus -> analysis), and half of it is coming up with the correct definitions (metaphors). Is it all that medieval? (Ironically, the medievalist recognizes that logic made great progress in that era, then took a break in the Renaissance until Frege and friends)

One of my favorite professors started the year by telling us that the only equipment we need to work on computer science problems is a pencil and some paper.