Was reading my birthday book on Chaos last night before falling asleep. Again. ...
I think maybe I've finally put my finger on a satisfying (to me, anyhow) explanation of why the Dijkstra/Wirth/Hoare/... program-correctness proof stuff hasn't had any real impact.
Computer programs can simulate any aspect of the real world to any desired level of accuracy. (Yes, we can quibble about that. Some other time.) In particular, say, they can simulate chaotic systems, as the weather simulations that spawned chaos theory do. Which means that computer programs can exhibit the same "sensitive dependence" which allows an arbitrarily small change in data -- or code -- to have an influence on the state that increases exponentially over time.
Taking a more general view of chaos, similar things can be true even in integer computations which don't fit the classical floating-point chaos model: Changes may propagate in ways that dominate the computation after awhile, and there may be no effective way to understand how they do this: With a nod to the Halting Problem proof, there may in general be no more effective way to understand the program than to run it, essentially.
I think what is going on is that a large fraction of possible programs just really aren't amenable to understanding. Even, or perhaps even especially, programs which perform interesting computations.
I think a crucial point to understand may be that the set of programs which allow the sort of maintainance which we would like -- in which desired changes of behavior can be implemented by local changes which are guaranteed not to destroy other desired properties of the computation -- are a very tiny and exotic subpopulation of the total space of programs. In some sense these programs must be "orthogonal", decomposable into linearly separable components which compute different parts of the desired result without interesting interactions.
There is no a priori reason to suppose that a given computation must have an orthogonal representation: Quite likely many interesting computations just don't have such representations, or when they do, the orthogonal representations are so much larger and less efficient than the optimal representation as to make them of little practical interest.
So, ultimately, efforts to enhance the reliability of programs may well have to bifurcate into two quite different approaches: Study of orthogonal programs, and understanding what results they can compute, and study of non-orthogonal programs, and understanding how to cope with their inherent instability in the face of change.
The existence of weather forecasting programs which consistently exhibit chaos would seem to establish that there _are_ important classes of programs which just are plain are _not_ subject to tidy proofs which establish the properties of interest and the new properties of any simple modification of the program, or conversely the modifications required to achieve any simple change in properties of interest.
Whether this is very exceptional in practice, or whether it is ubiquitous to the point of dominance, is an empirical point which remains to be resolved. But we may well have here yet another of the important limiting sorts of theorems which characterize this century: Heisenberg's Uncertainty, Godel's Incompleteness, Chaos...
It may be that the holy grail of software components which plug together linearly to exhibit predictably just the properties we want is a chimera, that for most practical programming problems there simply _is_ no way to linearly sum code fragments possessing individual desired properties to produce a complete program possessing the complete specified property set, that there -is- no general technique for adequately combining such parts that doesn't involve something akin to simulated annealing, painfully propagating mutual requirements back and forth and adapting each existing module to the added constraints imposed by the new context.
I don't see a quick way of proving this, but it feels intuitively about right, and it is quite consistent with the state of the computing field: It would explain why the brightest minds in the field have failed for half a century to discover the magic bullet that makes programming simple and mechanical, why plug-in software components are forever promised but never seem to deliver, why the people achieving the practical programming results, like Larry Wall and Richard Stallman, form a disjoint set from the people devising "scientific" ways of programming effectively.
There must certainly _be_ a class of orthogonal computations and programs: Dijkstra & Co may wind up identifying it fairly clearly in the end ... and may well find that, like the class of analytically solvable equations, it forms a small set of toy problems pedagogically useful but almost irrelevant to real practice.
Where would practical engineering be today if engineers limited themselves to designs which are analytically tractable, avoiding all numeric computation? Possibly about where the software field would be if practicing programmers limited themselves to programs amenable to Dijkstra & Co's proof techniques? A few solutions for the two-body problem, and promises that three bodies will be supported "any day now"? :)
If this analysis is correct -- I'm inclined to bet that it is pretty close -- then neither proof techniques nor object-oriented techniques nor anything envisioning simple linear combination of software components into the larger structures that we need is going to get us very far: The simple truth is going to be that large software systems are hard to create and modify, that no silver bullet is going to make that difficulty vanish, and that the main longterm win is going to come from tools which help us tackle that difficulty head-on: Sophisticated software support environments which understand as much as possible about the software parts stored in them, and which can help with the process of propagating constraints created by new juxtapositions, detecting resulting constraint violations, proposing and trying different ways of resolving them... Visualize simulated annealing performed on a large sofware system by a man/machine team, and you may have the basic paradigm for the best that is possible in the general software development process.
A related but not quite identical insight:
Since we can, and really do, use software to simulate or interface with any part of the universe which is of interest to us, it follows that the set of concepts which are relevant for understanding our software includes all those concepts which are relevant to understanding our universe. And more, since we use computer to invent new universes as well.
Hence, if a programming support system is to be capable of understanding most software systems well enough that talk of "correctness" and such become relevant, it must be capable of understanding most of our universe as well, and possibly a lot more besides... Computer science in the Dijkstra & Co sense can't be much simpler than the entire scientific enterprise. No? (If "correctness" is taken not to include this sort of stuff, then it will inevitably exclude most of the properties of programs that make them actually useful, and cannot possibly address the "software crisis".)
This means that a really effective software support system has to tackle all the issues of knowledge representation and such that Artificial Intelligence has been butting its head against for years with negligible positive results (albeit lots of results in terms of learning to appreciate how difficult lots of apparently simple things are).
Being brutally practical about it all, it appears to me that the bottom line is that seriously effective programming support environments that let us rapidly construct reliable programs represent a problem which is as difficult as artificial intelligence >just for starters<, hence that we're not likely to have them until after we have intelligence working... and that once we have intelligence working, there will be no point in having humans write code anyhow, except as an artistic statement or such.
In sum, a problem to go around rather than attack head on, at least for me personally.
As a minor aside, Dijkstra & Co, when they aren't too busy complaining that everyone isn't using their approach yet, will admit that they've not even begun to tackle the problem of large programs. Their defense is that large programs are made of small chunks, and thus that understanding construction of small chunks is a necessary prerequisite to tackling large programs.
Aside from demonstrating yet again how very far we are from anything -like- a plausible scientific programming methodology, this argument appears to me to be quite bogus. This doesn't mean that its conclusion is incorrect, but I don't think that it establishes that conclusion:
1) The simple truth is that from a practical point of view, there is no evidence that writing small chunks of code is a problem. Beginners do it from day one. Any particular chunk of code from a big system is usually easy to understand per se, devoid of the sorts of problems which justify the programming-in-the-small proof techniques. Even people like Knuth who are thoroughly familiar with these techniques seldom use them in practical programming situations -- skim the source for TeX.
2) As my father pointed out to me, there is no need for structure on one level to depend sensitively, or even at all, on the structure on a lower level. A program will run the same whether the computer is implemented in vacuum tubes, bulk bipolar transistors, MOSFET VLSI, Josephson junctions ... or tinkertoys. Complete mastery of quantum theory need not be of any help whatever in understanding that program.
Correspondingly, there is no a priori reason whatever to believe that dealing effectively with programming-in-the-large will benefit in the slightest from study of programming-in-the-small, nor that programming-in-the-small techniques will be of any benefit whatever in solving the "software crisis".
3) We routinely build structures without a clear understanding of the smaller scales involved. Mechanical engineering got a _long_ way before the existance of atoms was even established, much less before any quantitative understanding of atoms was achieved. Furthermore, most of mechanical engineering wouldn't even be _possible_ today working directly from "first principles": We still have no practical alternative to the bulk-matter theories for most bulk-matter problems.
There really is no reason to believe that solving the problems of building large software systems depends >in any way< on solving the problems of building small ones, that solving either will shed light on the other, or that the solutions will be in any way related in form or theory.
Industry statistics argue compellingly that the 'software crisis' is one of large software systems, not of small ones. The spectacular failures are large systems and the overruns and chance of cancellation rise dramatically with size. There's no compelling evidence at _all_ of a software crisis in the field of one-line programs, for example: Millions of people produce them on the fly daily in an enormous variety of different shells and applications, with no great cry for higher productivity. (There is _some_ demand for higher reliability, to be sure. "I just lost all my files. What do I do?" :)