controlling resource usage

D. Tweed
Sat, 8 Sep 2001 19:50:56 +0100 (BST)

On Fri, 7 Sep 2001, Jon Fairbairn wrote:

> > 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.

You might be right; I just have nasty 5 year old memories (that my
subconscious hasn't succeeded in suppressing :-) ) of trying to coax OBJ3
to perform proofs on very simple things and finding it so difficult that I
can't imagine it being usable by a programmer with no intrinsic interest
in the logic process without some extreme advances (which may just be
increasing processor capacity so limited application of `brute force'
approaches become more feasible). In some ways I suspect that Knuth's idea
may be simpler to implement than yours in that there all the creativity
and optimization is performed by the programmer; the computer just
(very reliably) ensures equivalence between the two versions of the 
program and (with vague reliability) tries to alter the optimised program
as small changes to the original are made to preserve semantics but
not necessarily efficiency.

But I'll certainly be keeping an eye out in the future for a system of
either kind that I can use in my programming.

___cheers,_dave________________________________________________________ |tweed's law:  however many computers
email:      |   you have, half your time is spent
work tel: (0117) 954-5250       |   waiting for compilations to finish.