due to cache coherency issues.) In that context, there was an old suggestion of Don Knuth's that program source code should in the idealized future not just contain the final, optimized code (with perhaps the original code in comments) but as a kind of set of layers each representing the same semantic program but with increasing orders of optimisation, and links between `things' annotated with a label placed by the programmer explaining why the transformation between an unoptimised version `thing' and an optimised `thing'.
[snip]
I suspect that such a system is still at least 25 years away from feasiblity though :-(
That seems to me to be an overestimate. One of the things I've had at the back of my mind since just after I faded from view (as it were), was a kind of formalised hand compilation. The background is that an automatic programme transformation system never knows as much about the problem as the programmer, so it has little chance of making the right decisions. In addition, of course, the prerequisites for certain transformations are undecidable. As a result, although research has been done on automatic programme transformation for a long time, people still rewrite programmes by hand. The same applies to ordinary compilation (after all, compilation _is_ automatic programme transformation): strictness analysis is fine, but if your programme needs strictness and the compiler can't spot it, you have to annotate by hand anyway. So, roughtly speaking, the idea is that a programme would consist of two objects, the unoptimised source code, and an optimising compiler written specifically for that programme. Obviously we'd provide default_compile, so that to begin with one would need do nothing special. Then we'd want a way of breaking down the compilation into individual functions, for which we could specify different compilation strategies. For example, if f [] = ... f x = h x ++ f (g x) we might specify compile f = default_compile (eliminate_append f) (Not sure what the syntax should be, or how to specify to which function a new rule applies) At the back of my mind is something like the way proofs are constructed in HOL, though I'm thinking of a system where the ordinary programmer doesn't write new optimisations, just gets to select which ones are used on which bits of the programme. The optimisations can be fairly dull and complain if the function to which they are applied doesn't match their pattern. Producing new optimisations would be a task for a guru, probably armed with a proof assistant. Not that there's any law that some programmers can't also be such gurus, of course. I'm certainly not in a fit state to have a go at this myself, but I'm sure there's lots of stuff from the programme transformation and proof assistant worlds that could be applied here, but with the advantage that it doesn't have to work automatically. There's also scope for permitting the application of transformations that may be only partially correct -- we have that with $! already. I'd want the compilation and optimisation stuff to be kept in a separate file from the programme itself, but would ultimately hope for tools that allowed the two to be manipulated together. I tried mentioning this to a beginning PhD student a number of years ago, but somehow it didn't excite him. Maybe someone out there has a vision th t more closely matches mine? Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk 31 Chalmers Road jf@cl.cam.ac.uk Cambridge CB1 3SZ +44 1223 570179 (after 14:00 only, please!)