David Hilvert
Wed, 28 Jun 2000 11:39:45 -0700 (PDT)

Proposals for new or different ideas seem to sometimes meet with hostility
or indifference on this list, as they do most places, I suppose.

Specifying program behavior is a significant part of what TUNES is about,
in my view.  Look at section 3.12 (Program proof) of Fare's "Why a New
OS?" paper, for example (there may be better examples).  

I have been fairly impressed by the amount of work that has gone into the
HLL candidate Slate.  Its recognition of the importance of namespaces is
important, I think.  I have not heard from Brian or anyone else much in
the way of detail as to how the user may specify program requirements for
Slate, but I suspect that Brian considers this to be important, so perhaps
you might ask him about it.

In any case, Slate is not the final candidate for the TUNES HLL, so
you are of course free to propose other ideas (and especially

I must say that I am somewhat skeptical of the practicality of generating
all possible implementations of a specification.  Perhaps you could
clarify what you mean or go into more detail.  I may have misread what you