Don't hardwire OS features

[Francois-Rene Rideau]

>>: Fare
>:Alaric

>> 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.
Well, see the Coq system about how a good proof system
(but not remotely a reflective OS) does it.

>> * 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.
Yes, but the contract is not computationally checkable at runtime,
like the Eiffel model requires contracts to be...

>> * 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!

>>    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!
That's the ideal case where everything is proven
but for a small "kernel".
Not for early releases, unhappily.

>>    Only, doing that in Eiffel would mean explicitly and manually
>> reifing the proof system,
> "Reifing" = ?
Well, I meant reifying, of course.

>>    Remember: every one is free to run code that
>> has not been proven correct with respect to all its specifications --
>
> Beware the ActiveX trap :-)
>
What is this trap already?

>> 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) ;-)
>
Oops :-( I meant 2*2^(2^512)=2^(2^512+1), of course.
And this means that even automatic inline expansion of integers
should be a short-circuitable tactic:
if you try to expand the previous numbers to verify the equality,
you'll never have enough memory in the Universe for that,
and even less time!
The good side of it is that whatever the proof system "kernel" is,
it will be very small, as it should.

> 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...
Well, more simply, there is no kernel that checks anything;
yet, all the usual ways to add new code go through a code checker.
This can be compiletime, linktime, runtime, or whatever
(the spacerocket code would better be fully checked before runtime,
if we want to avoid yet another $10G crash!).
That no kernel does it does not mean that it ain't done.
Compare OS "kernel" and State:
that the State doesn't grow crop
doesn't mean that no one grows crop,
and that everybody starves;
rather, it means that there can be a fair market for crop,
that will allow adaptation between user needs and producer capacity.
Similarly, that the kernel doesn't check proofs itself
doesn't mean that things won't be proven;
rather
The rightful role of State is to ensure that Law will be followed,
that contracts will be fulfilled,
that common resources will be fairly multiplexed;
even then, it should delegate its powers rather than centralize them.
The rightful role of the OS Kernel is just the same,
in the limited scope of the computer world.

> --
> Governments are merely protection rackets with good images.
Perhaps they are, but they needn't and shouldn't be.
If governments were restricted to their rightful role,
and stopped any kind of Welfare state by privatizing
welfare institutions
(making tax payers share owners, and/or making independent foundations,
rather than giving away common ownership to private commercial groups
managed by personal friends of the current leading party,
transforming state monopolies into private monopolies),
they wouldn't be such rackets.

== 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/"