3 ms·
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 arg
by panarky 5y ago
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.
- jhanschoo 5y agoYes, 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)