Don't hardwire OS features

[Francois-Rene Rideau]

>: Alaric
>>: Fare
>>>: Alaric

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

>> Also, building a specification system with the belief
>> that automated proofs are possible independently of specifications
>> is illusory.
> Specifications of what? Many things are 'specified' in Eiffel.
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!

>>> That can be done quite easily, IMHO. Enumerate the things that cause 
>>> crashes, and mask them off.
>> No, that can't be. Because there are infinitely
>> many things that may cause crash,
>> and masking them off is not computable.
> 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.

>>> I mean, a mathematical system for converting from syntax A to syntax 
>>> B, with the /maximum/ efficiency possible. As in, if syntax A is a 
>>> turing machine, and syntax B contains a simple instruction for most 
>>> of what a neural net does, then a neural network implemented in A 
>>> will use this instruction in B. IE, the ultimate compiler will be one 
>>> application of a fundamental theory of computation!
>> No need for a lot of fundamental theory to show that
>> such thing is not computable.
> Maybe not always computable, but if we place reasonable restrictions 
> (like, all of our semantic contructs can be represented by a finite 
> piece of code in another syntax) then it looks easier. But only 
> /relatively/ easier :-)
Not even. Reducing a form to the maximum efficiency possible
means that in particular we can detect a function that always returns 0,
to translate it as a program returning 0 immediately,
which is known to be a non-computable task.
Placing restrictions on programs is what most people do,
and only ends up in bloated restricted systems of limited utility.
   The Tunes philosophy is that people will reflectively push
the limits ever further, by being able to dynamically
redefine and extend the translators...

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

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

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