Don't hardwire OS features

[Francois-Rene Rideau]

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

>>> 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.
See around http://www.inria.fr/ and
ftp://ftp.inria.fr/INRIA/Projects/coq/

> 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.
We'll see.

>>> "Reifing" = ?
>> Well, I meant reifying, of course.
> Yes, but what do you mean by that, no matter the syntax????
Glad to have you ask that: meaning, not syntax.
Well, that's basic reflection vocabulary:
Reifying an object means taking a manipulable representation for it.
The reverse operation is absorbing a object,
which means adding a new feature to the system
by making such object part of it.
Typically, you implement system layers
by reifying objects, (re)writing code,
and absorb the object back.
   For instance, if I want to manipulate a database,
most of the time I don't care the format in which it is implemented;
what I care about is being able to manipulate the database at will,
and be able to exchange data with my partners.
Hence, I want it to be abstract, not concrete,
and I *don't want* to reify it;
but low-level C programming will require me
to manually manage the format, conversion, etc,
be it line-oriented ASCII text (yuck), db/dbm/dbz/whatever format,
or proprietary stuff.
   But sometimes, I want to manipulate the representation,
to modify the implementation, so as to optimize it or add features
(persistency, distribution, specialization, etc).
These means that I'll have to *reify* the given objects.
Non-reflective systems (e.g. C) won't allow me to do that,
unless I work on the reified version from the beginning on,
without being able to change the way I represent things
but by a complete rewrite of the code.
Reflective systems (Scheme and LISP object systems,
Smalltalk, SELF(?), Dylan(?), and other) do allow reification,
with their so-called meta-object-protocols.
But I want it to be done consistently,
in a way that I'm sure that if the representation is changed,
the abstract data is conserved.
And these systems won't provide the beginning of the shadow
of any consistency check.
   That's were Tunes come:
letting people be free to reify or not.
But Freedom is not basing one's choice on randomness,
relying on chance, praying to be lucky;
Freedom is basing choice on knowledge,
taking responsibility.
Being free to reify means
being able to *know* that your reification is correct or not.


>>>>    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. [...]
> 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!
Yeah, with these systems, you are not free to run unsafe code or not,
you're bound to run *their* code or run no code.
You're not free, you're their hostage.
Well, just the continuation of the very principles on which they live,
that they want to extend to dynamic network-passed code.


>> 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!
>
I admit I didn't invent anything about the State.
I just draw the (limited, yet powerful) analogy
between State and the OS Kernel:
in both case, the ultimate authority
between parts of a dynamical system.


[Cut from here to "!!!!!" to avoid political chat]
>>> 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!!!!
>
That's a shame! While exploitation and maintenance of railway lines
should indeed be privatized, the lines themselves should be public,
because they are ground that was taken from the people with promise
to help them travel, just like streets, roads, rivers, seashores, etc.
Privatization is made to allow competition.
What competition can there be
when there is a monopoly on the infrastructure?
I see only local non-competing monopolies.
Requiring competitors to build a parallel railway network
is an insult to fair competition.
Forbidding it would be a similar insult, too, of course.
   The same holds for the water industry:
water plants and pipe maintenance should be privatized;
but pipe property should be public,
or else we have a monopoly.
Maintenance of street and roads must be private;
streets and roads ownership must be public.
Please note that public doesn't imply centralized/owned by state,
which is more like the subject of the Tunes project.
Centers for treatment of pollution should be private;
the air itself, nature, the sea, rivers, etc, should be public
When will state privatize air?
you'll then have to pay a fee to company to have the right to breathe!
   The Rule is: anything that is shared by everyone should be public owned.
Everything else (including maintenance of the former) should be private.
The problem is: statesmen don't respect this rule at all,
and welfare state has corrupted the notion of state,
in the same way than tyranny would:
rather than being a warrant of public and private ownership,
State as they see it is some kind of active company,
that feeds from a huge racket named taxes,
and must spend more than all of this income to
enrich themselves and friends, and corrupt people in voting for them.
They have no notion of public-ownership, only of state-ownership,
of which the ruler can dispose at will, as an allmighty tyrant.
To them, democracy is not a way to be free,
but a way to choose and limit a tyrant.
Anything that the state holds to them could be potentially
sold out to their friends, if only the public wouldn't
demonstrate against in the streets;
meanwhile, they can manage it as their private property,
as long as the public sees nothing of how they take the money away.

["!!!!!" -- end of political chat]
[political followup to private e-mail,
unless it has computer consequences, as is the case here]

To come back to the computer world,
wild privitization would be like letting Microsoft and/or various
companies buy the Internet and control it completely,
(so that for instance they could decide that
everything you write being their property if you publish it,
or more humbly that you'll have to pay their racket
for the right to exist),
and you would just have to rebuild a parallel network,
and all the infrastructure, if by chance you disagree.
   Surely, nodes should be private, and in the case of the internet,
most cables should be private,
in as much as competition is most often possible about them cables.
But the protocols and meta-protocols should be public;
the information should stay ownership of its authors,
it shouldn't be possible for any company
to decide who can be connected or not,
to impose a racket fee for entrance in the world.
   All services should be provide by private companies;
but the standards according to which these services are rendered
should be public.
Sometimes, these services are to gather a large public database;
then this database should be public, and the provider must be
subject to either competition or control by possible revocation.
   As a example, let's take proof checking.
It is surely not the role of a centralized "State" agency
to check for proofs. Yet, everyone will benefit from
not having to ever recheck the same proofs for the same software
(loss of network, CPU, and disk resource multiplied by
the number of users -- ouch!).
Hence, you could very well have proof checking companies
that would provide synthetic signatures for checked programs,
or simply signatures and hard money guarantee on failure.
Companies that sign without providing either proof or money guarantee,
as Microsoft pretends to do, will be laughed at.
Companies that pretend to sign for proof must themselves prove
their statement. Again, a meta-proof and/or money guarantee
will naturally be required by a fair competition!
Of course, the proof standards should be public,
else they be valueless.

> Thinking of that, I could come visit you some day via the Chunnel
> (I'll wear breathing apparatus and an asbestos suit).
Sure! You'll be most welcome!
But beware that most of the time this year, I'll be in Nice, not Paris:
a nice city too, but further south;
but tell me the day you cross the channel in such an apparatus:
I'll be waiting for you at Calais!

> That way, you could /draw/ me a proper epsilon symbol...
I'm sure you can find easier ways to solve this problem...

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