Don't hardwire OS features

[Francois-Rene Rideau]

>>>: Alaric
>>: Fare
>: Alaric
>
>>>[limited specifications in Eiffel]
>>> The extension beyond assert() is that they have an "implies"
>>> boolean operator, the import of which is not clear. I have seen
>>> written: "divisor /= 0 implies Valid()" and things like that.
>> This means that Eiffel can manage several kinds
>> of possible assert() for a piece of code.
>> More powerful than assert(), but not much more expressive.
>> Quite far away from full specifications that would allow
>> to statically check for program correctness.
>
> 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.
* such variable will not ever be modified after being initialized
* 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...
* I want my code to behave exactly like such other (legacy)
 code in the following "normal" conditions.
* 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).
* Such parameter function must be a bijection from type T to type U,
 and such other parameter must be its reverse bijection.

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).
   However, any code that runs must have a proof given
(a superuser "admit it" statement being a proof, of course);
hence, you would like to say that we are not much more
expressive that one that allows only explicitly checkable assertions,
as in Eiffel.
   Only, doing that in Eiffel would mean explicitly and manually
reifing the proof system,
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).
Hence, big shit.
   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.


Of course, building any of these specifications from scratch
might take pages and pages of logical code.
But not more pages than what require all dumb manual checking
that security without proofs would require.
And proofs and specs are reusable as modules,
consistently combinable and upgradable, etc,
whereas manual checks are not.
   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.
   Remember: every one is free to run code that
has not been proven correct with respect to all its specifications --
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) ?

== Fare' -- rideau@ens.fr -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"