Don't hardwire OS features

[Alaric B. Williams]

On  8 Dec 96 at 1:50, Francois-Rene Rideau wrote:
> >[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.

What would one need to implement that, then? Giving an example....?
 
> 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.

Eiffel is strongly typed, anyway!

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

But I'm designing a new language anyway...

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

Why not? Computers are finite... If we can prove that none of the 
basic programming constructs will ever crash - possible, since they 
all do simple things - then no combination thereof can ever crash.

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

It can be implemented purely as a small set of classes (Key, 
ColourKey which inherits behvaiour from Key Lock, 
and ColourLock which inherits behaviour from Lock)

> * 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).

Indeed. The standard way of implementing the security system would be 
by passing a key during the opening of a channel between two 
entities. The target entity only allows some channel types to be 
opened if a good enough key is presented.

> * you can build all the layering you dream about,
>  and much more as libraries over the modular Tunes design,

Both will be implemented as classes in the object oriented ARGON 
design :-)

>  whereas the converse is not securely possible.

Why not?


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

Alaric B. Williams Internet : alaric@abwillms.demon.co.uk
<A HREF="http://www.abwillms.demon.co.uk/">http://www.abwillms.demon.co.uk/</A>