4 ms·
It is funny how this paper like the writings of Dijkstra is widely cherished, while its attitude and conclusions simultaneously are completely ignored. Seems to
by stiff 12y ago
It is funny how this paper like the writings of Dijkstra is widely cherished, while its attitude and conclusions simultaneously are completely ignored. Seems to me that people simply really like to complain about the current state of the matter, how dirty programming is and how everything is inelegant just to get back to churning code a minute later using exactly the style criticized.
People like Backus and Dijkstra really wanted to prove theorems about programs and do formal derivations like they were used to do in mathematics, that's practically all they cared for, as far as their writings go. The "liberation" is in fact an act of bondage, an attempt to limit programming techniques to a narrow range to try to get all the noble benefits of mathematics, which is a priori assumed to be the best way to go about reasoning. It's really ironic in the case of Dijkstra, who writes about how people cannot appreciate "radical" novelties and instead keep old mental habits, and then proceeds to argue how programming is just a branch of mathematics.
I wonder how many people who mention those papers as cornerstones of CS actually prove their programs correct on a daily basis or derive them from "axioms". I actually think many people in the formal methods camp had a very narrow and limited vision of what programming is and what it will be become, and as a result turned out to be very much wrong about the importance of proofs in programming. Some of them actually admitted it:
http://www.gwern.net/docs/1996-hoare.pdf http://www.gwern.net/docs/1996-hoare.pdf
In the end, reducing all programming to formal manipulations of this kind turned out to be as successful as the ideas of axiomatization of biology. Formal methods are useful in mission-critical software, functional programming penetrated mainstream languages and is interesting in its own right, but even its proponents hardly go about writing programs the way Backus imagined; mathematical theories of programming turned out to be very limited and yield poor crops compared to the mathematical theories that turned out to be successful, hardly any new insights over what was found earlier by dabbling were found, and that is that. I love math, but it seems that programming, like biology, is actually richer than math in some sense. Consider the example Peter Norvig gives in "Coders at work": how do you prove Google is correct? You immediately run into issues with the very notion of correctness, not everything can be convincingly formalized to the last detail, and we build more and more of those "fuzzy" systems, just consider the rise of machine learning and data mining in the last years.
I see no reason to go around pretending programming didn't live up to the noble vision of the ancient masters. The masters were frequently wrong (no shame for they were pioneers of the field and nothing was known), and we simply moved on.
- loup-vaillant 12y ago> Dijkstra […] then proceeds to argue how programming is just a branch of mathematics. Which it is. In a trivial sense, programming languages are formal systems. Even when poorly specified, the computer they run on is a formal system. In a less trivial sense, we have the Curry-Howard correspondence. In a very real sense, programming language designers have denotational and operational semantics. Fuzzy systems need not get rid of mathematics. They just switch from first order logic to probability theory (or a computationally tractable approximation). Ignorance of basic mathematics is why so many fools believe lambdas or monads are hard to understand. It feels like we're scared of abstractions. For instance, we solve linear equations every time we go to the grocery and pay cash. Yet being presented with those linear equations as such, get us running away screaming into the night. --- Programming is applied math, period. The question is, which kind of math do we want to use? Which are the more useful notations, formalizations, theorems? How does all that relate to the old math?
- seanmcdirmid 12y agoIn a trivial sense, life is a formal system. Even when poorly specified, the universe we run in is a formal system. Everything is then math, period. The question is, which kind of math do we want to use to reason about life? Hey, when you figure it out, let me know.
- dagw 12y agoI disagree. Computer Science might be a branch of mathematics, but computer science is also just a part of programming. Programming also involves things like software design and engineering and human computer interaction which are not a branch of mathematics. Programming is like building a bridge. Yes lots and lots of math is involved in building a successful bridge, but claiming that bridge building is just a branch of applied mathematics is kind of missing the forest for the trees.
- loup-vaillant 12y ago> Programming is like building a bridge. Not quite. When you build a bridge, you'd better doing according to spec, or it will collapse. The specs better be sound according to the known (mathematical) laws of physics, or it will collapse. Lot's of theorems to use, and lots of proving your design is sound. Software is often more lenient, and as such less mathematical than bridge building. But that doesn't help my point. How would you go about proving a mathematical conjecture? You think, you talk to colleagues, you try approaches, you design tools (notations, programs that do math…). That's less formal than you might think. Heck, the proof you provide in the end is often not even machine checked! Coq users are often more rigorous than the most die hard mathematician in this respect. Just like software writing and bridge building, the process of doing math is not mathematically formalized. In that sense, there is a lot more to math than math.