Don't hardwire OS features

[Francois-Rene Rideau]

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

>> Well, specifications of the programs you write!
>> There is no way in Eiffel for the programmer
>> to specify proofs that the
>> pre/post-conditions will actually be satisfied.
>> Hence, the compiler if anyone/anything
>> is entirely relied-upon to prove it,
>> which I pinpointed was an illusory assumption!
> If that becomes a problem (when somebody starts to write a 
> static-checking Eiffel compiler) then syntax for inserting proofs 
> like that can be defined!
No! It's even worse than if you said that a syntax for types
could be added later to assembly or C.
It's easier to strongly type an arbitrary assembly/C program
than to prove an arbitrary Eiffel program correct.
In any case, this would mean that all Eiffel programs
would have to be completely rewritten, and then I wonder
why people would stay with that &@%*!$ language.

>> there are infinetely many possible
>> cases of crashes, corruptions, hogs.
>> You just can't enumerate them to mask them off.
> Hmmm. If the hardware is reliable, exceptions such as stack overflows 
> are handled correctly, and interrupt handlers behave correctly, then 
> surely if we make sure pointers (both code and data) always point to 
> valid places (including inside array subscripting) - and our GC works 
> - then how can anything crash?
This is *not* enumerating all possible crashes and masking them off.
Possible crashes are not even enumerable.
This is specifically using constructive proof techniques.
Welcome among computer program proof checkers!

>> Being at the same time "low-level", "portable" and "efficient"
>> means lots of bloat anyway...
> How would you implement things like that, then? :-)
Tunes does not pretend to solve contradictory goals.
What it does is allow to dynamically adapt the means to the goals,
instead of making a static uninformed compromise.

> I'm wondering which is more useful: keys form a hierachy
> or to have each colour cover a seperate view of the object.
Whatever it is
* this can needs no more HLL/OS support
 than static binding and scoping of views on objects.
* to be useful, views on an object must reflect the semantic structure
 of the object, adapt to object. Building an arbitrary static hierarchy
 only leads to unadapted design (see VMS bloat).
* you can build all the layering you dream about,
 and much more as libraries over the modular Tunes design,
 whereas the converse is not securely possible.

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