Don't hardwire OS features

[Alaric B. Williams]

On 15 Dec 96 at 1:00, Francois-Rene Rideau wrote:

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

Hmmm... can you recommend a good webpage or such document about it? 
I'd be quite interested.
 
> >>    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.

Depends how you develop, I guess. I'd have my basic operation set 
worked out, and get that debugged before starting to define things in 
terms of them.
 
> > "Reifing" = ?
> Well, I meant reifying, of course.

Yes, but what do you mean by that, no matter the syntax????
 
> >>    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?

ActiveX controls are Microsoft's idea of a competitor to Java. They 
consist of - basically - 32 bit DLLs which are fetched accross the 
'web. Despite the Godawful portability (pick: Intel-based Windows or 
emulated Intel-based Windows...), the idea of transparently 
downloadable raw object code pumping into an insecure OS should send 
any sane computer scientist around the bend. Well, Microsoft claim 
ActiveX is secure because ActiveX controls are public-key certified 
by "trusted authorities". Thing is, those trusted authorities tend to 
be big companies. Would you trust a control signed by an unheard of 
company? Nope. Also, you're trusting this authority not just to 
produce a control that isn't a Trojan Horse program, but to be /bug 
free/. Because once you start a heavy stream of executable code into 
your system, that chance of you meeting that hard disk wiping bug is 
that much higher.

So, basically, the major flaw with ActiveX is that it thinks that 
trusting electronic signatures or other such assertions of 
reliability is a good substitute for transmitting code in analysable 
form!

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

Uhuh :-)
 
> > 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.

Nicely put!
 
> > --
> > 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.

Yeah, the problem we're getting here is that the govt. are 
privatising everything. Look at our rail system!!!!

Thinking of that, I could come visit you some day via the Chunnel 
(I'll wear breathing apparatus and an asbestos suit). That way, you 
could /draw/ me a proper epsilon symbol...

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

Alaric B. Williams Internet : alaric@abwillms.demon.co.uk
http://www.abwillms.demon.co.uk/