controlling resource usage

[Lindsay Errington]

"D. Tweed" wrote:

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

Kestrel's Specware system aims to be just that. One begins with abstract
specifications in higher-order logic. You then apply semantics-preserving
refinements to yield concrete code in an executable subset of the specification
language (a pure functional language). Like OBJ3, Specware is coupled to a
theorem prover to discharge proof obligations that arise along the way. As you
point out, expecting the machine to be creative is optimistic, so instead,
program synthesis is driven by the user selecting and instantiating abstract
algorithm schemes (eg divide and conquer) from a taxonomy. A modest amount of
category theory ties everything together. It provides the basis for refinement,
parameterization and the structuring and composition of design knowledge. You'll
find more information at: http://www.kestrel.edu/  but note that we are in the
process of updating our web pages.

You've mentioned an idea due to Knuth. I would be grateful if you could send a
reference to  it.

Best wishes,

Lindsay