Don't hardwire OS features

[Alaric B. Williams]

On  7 Dec 96 at 0:05, Francois-Rene Rideau wrote:

> From:          Francois-Rene Rideau <rideau@ens.fr>
> Subject:       Re: Don't hardwire OS features
> To:            alaric@abwillms.demon.co.uk (Alaric B. Williams)
> Date:          Sat, 7 Dec 1996 00:05:47 +0100 (MET)

You're up late!

> >>> Eiffel was designed so it is possible to prove things, just no 
> >>> compilers do much proving beyond type inference. So Far.
> >> Surely I should re-read more in detail the Eiffel specs.
> >> But from what I know of Eiffel practice,
> >> only computable checks are used as pre/post-conditions,
> >> which severely limits the expressiveness of the specification system.
> > Hmmm. I'm not sure which restrictions apply. But surely they can be 
> > relaxed...

> The restrictions, as I understand it, is that
> pre/post-conditions in SELF are essentially the same as assert() in C,
> just that they are placed at the beginning and end of code blocks.
> Hence only simple computable conditions can be used...

Eiffel, not SELF :-)

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.
 
> 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!
 
> > I'm not considering going into infinite loops as crashes here; they 
> > only affect the affected application. I'm talking about 
> > corrupting/hogging system resources. If we can prevent that, 
> > applications are welcome to nosedive as long as they don't take 
> > anything else down!

> I'm also talking about the same.
> And I'm saying that 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?
 
> >> ...you can copy the asm/*.h from Linux,
> > Final point: then the developer has all the horrid work of dragging
> > around possibly unnecessary (if it's compiled on Linux in the end)
> > utility code with his product! What if he'd used a real /big/
> > 'optional' feature??? This problem still remains mostly unexamined as 
> > far as I see...
> Well, who said C was not a bloat-oriented language?
> Being at the same time "low-level", "portable" and "efficient"
> means lots of bloat anyway...

How would you implement things like that, then? :-)
 
> >> You biggest security problem is likely to be with traitor commie mutants...
> > (puzzlement)
> Well, you security classification by colors is exactly
> the same as in the RPG "Paranoia", apart that their
> lowest grade is infrared, and their highest is ultra-violet...
> The motto of paranoia: "The computer is your friend" ;-)
> Unhappily, there are lots of traitors against the
> benevolent rule of the computer on the alpha complex,
> so you must be on your guards, because this guy near you
> could be one of them! Or perhaps he's not and that's worse,
> because he knows that *you* are a traitor!

Ah... I see :-)

I'm wondering which is more useful: keys form a hierachy (an orange 
key does everything a red one does, and maybe more), or to have each 
colour cover a seperate view of the object (which would require more 
colours). I guess I can offer both, using two kinds of locks... every 
key now has a name on it; a ColourLock takes keys with names like 
"red" or "indigo" and returns the colour if the key is correct, a 
mere Lock takes a key and returns the name if the key is valid.

So if a key is coloured, the user knows it fits the hierarchical 
system, etc. If we have nonintersecting key functions, then multiple 
keys may need to be specified for one operation. Which makes some 
things less simple.

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>