Don't hardwire OS features

[Alaric B. Williams]

I've joined the Tunes list now, so you needn't CC stuff to me anymore 
:-)

On 14 Dec 96 at 14:28, Francois-Rene Rideau wrote:
> > So what would "full specifications" look like?
>
> They would look like saying that
> * the sort function will take as parameter
>  a function from a totally ordered
>  finite set to a totally ordered set,
>  and compose it to its right with a permutation
>  of the departure set,
>  such that the resulting function be non-decreasing.

Hmmm... the syntax for this kind of thing could be quite manly.

> * such variable will not ever be modified after being initialized

I can handle that :-)

> * my code relies on a few memory access primitives
>  (say, malloc, getmem, putmem) to implement a GC'ed space,
>  without implementing the GC itself.
>  The user can give to it a GC as parameter,
>  but this parameter will be checked to actually
>  implement the expected semantics of a GC...

The GC parameter is good 'ol programming by contract, I guess.

> * I don't care how it does it (as fast as possible I hope),
>  but such module must correctly implement such language
>  (e.g. a database query system, a symbolic algebra package, etc).

Well that subdivides into proving that the language interpiler can 
be fed action semantic sources and follow them correctly. A nonatomic 
proof!

> Typical specifications use arbitrary logic quantifiers:

> for all and there exists, which cause generic proof-finding to be
> an undecidable problem (well, checkable hence semi-decidable).

The normal logic notation stuff, if only we had upside down As and 
reversed Es on keyboards :-)

>    However, any code that runs must have a proof given
> (a superuser "admit it" statement being a proof, of course);

One hopefully only ever needing to be applied to the basic primitives 
that a superuser could manually prove!

> hence, you would like to say that we are not much more
> expressive that one that allows only explicitly checkable assertions,
> as in Eiffel.

Well better logic syntax would be nice, allowing better flexibility 
in specifying these computable proofs. Perhaps something like Prolog 
:-)

>    Only, doing that in Eiffel would mean explicitly and manually
> reifing the proof system,

"Reifing" = ?

> which would also mean passing extra proof parameters
> (that the Eiffel system would most probably be actually passed at runtime),
> without the system being able to ensure consistency between manually
> reified specifications and absorbed specifications (typing, etc).

I think I see what you mean there (try and be more concrete in giving 
examples, please! :-)

>    Actually, only allowing explicitly checkable assertions
> is how the underlying system will work. Only the system is *reflective*,
> hence all the proof stuff can be absorbed by the system
> that will relieve the user from the problems of manual reification,
> ensure consistency between all specifications,
> and optimize runtime proof checking away.

Right. 
 
> Of course, building any of these specifications from scratch
> might take pages and pages of logical code.

The basic specifications need only ever be done once. In my 
experience, the lower level things are the hardest to explain 
logically! Once we have simple logical expressions for "if the sort 
routine works", we [hopefully] are able to express higher level 
procedures more concisely!

> And proofs and specs are reusable as modules,
> consistently combinable and upgradable, etc,
> whereas manual checks are not.

Indeed! They should be closely bound to the respective code, 
obviously :o)

>    Once the most basic specifications have been written,
> together with their most common (partial) implementations
> (e.g. integer calculus, with fixed-width or variable-width integers),
> then we have a fair basis on which to work.

Right.

>    Remember: every one is free to run code that
> has not been proven correct with respect to all its specifications --

Beware the ActiveX trap :-)

> it is enough that the code is correct wrt the much more restricted
> specification that it will not crash the system,
> for which use of (a correct implementation of)
> a strongly typed language is enough.
> And even then, godly (super)users can avoid this failsafe proof requirement.


> BTW, can YOUR theorem prover prove that 2*2^(2^512)=2^(2^512-1) ?

No, because 2*2^(512) = 2^(512+1) ;-)

But anyway it wouldn't need to to prevent crashes. The proof 
mechanism the 'kernel' (or whatever you'd like to call it!) uses 
before running stuff is the very simple one of strong typing. The 
contracts attached to strings of code can be runtime checked like 
Eiffel, or run through a seperate program checker...


ABW
--
Governments are merely protection rackets with good images.

Alaric B. Williams Internet : alaric@abwillms.demon.co.uk
http://www.abwillms.demon.co.uk/