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.<p>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.<p>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:<p><a href="http://www.gwern.net/docs/1996-hoare.pdf" rel="nofollow">http://www.gwern.net/docs/1996-hoare.pdf</a><p>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.<p>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.