Tunes

[Francois-Rene Rideau]

[Notes:
* To Mr. Hamdani:
 I'm forwarding this reply to the Tunes mailing list.
* To Tunes project members:
 if I'm missing something, saying anything wrong,
 misrepresenting the goal of the project,
 as you see it is, or as you see it should be,
 please do correct me.
]

>      Dear Sir,
> After reading you examples, I still do not get the 
> main concept (Perhaps the example is too complex).
> Do you have short, small example and explain
> the main advantage of Tunes?
> Please use plain english, not technical term.
> Best regards
> (Hamdani)
> PS: I have degree in CS.

Well, perhaps the draft document for my WhyNewOS article
contains more ideas.
Let me try to sum up the main ideas.
I feel my explanations are not as simple as they should,
but I find no other way...


The main focus of Tunes is semantic-based reflection.
* semantic-based means that the system will only do operations
 that preserve the *meaning* of objects, rather than their representation.
 For instance, people trying to optimize programs are prone to
 introducing bugs, all the more when optimizing for parallel architectures,
 where things become ununderstandable.
    If the development tools were guaranteed to preserve the meaning
 during program transformations, developers would write the
 program specification once and for all, and later optimize
 the programs while being sure that everything's safe.
 Newer programming techniques (better GCs, distribution of objects,
 dynamic partial evaluation, etc) could all be safely experimented.
    Such guarantees are given in the form of logical (mathematical) proofs,
 that the system can check, and that can be required by objects.
 You don't have to rely on informal specifications checked by humans
 with lots of red tape (or simply unchecked):
 see the $10^9 worth crash of the Ariane V spacecraft recently,
 due to a software bug that formal proof checking would have pin-pointed.
* Reflection means that you can dynamically manipulate objects
 that manipulate other objects, and modify the system.
    It means that you can dynamically optimize your programs,
 adapt the system to your needs, define new implementation strategies
 and proof tactics, create sublanguages for specific uses, etc.
    It means the same language can be extended
 so as to efficiently do everything one wants,
 which allows you not to have hundreds of crippled
 application-specific languages
 that can't communicate with each other.
    Yet this Reflection being semantic-based,
 you are guaranteed that all such manipulations are safe,
 that people using different extensions won't be stopped or fooled
 by *syntactical* clashes between the extensions,
 but can safely interchange meaningful data.
    Reflection is also the only way that
 the proof system itself be proven correct, etc,
 with the set of axioms (that we know can never be empty) decreasing,
 rather than increasing.
    Ultimately, the whole of the system will
 have been proven correct with respect to a small list of axioms
 that can be trusted for being small enough and having been
 thoroughly tested by all the hackers in the world,
 this proof system kernel being widely used free software.
    Note that because a software system can't be more reliable
 than the underlying OS implementation, TUNES will eventually
 have to be a full OS: there's no point in having proven-correct software,
 if that software is to run on top of buggy Windows95.
    Also note that using minimal simple MISC hardware
 will allow to feasibly prove the hardware correct
 with respect to the physical model,
 whereas CISC hardware requires you to trust bloated designs,
 where you never know if there ain't a hidden bug (see pentium bugs).


Tunes also promotes
* orthogonal persistence
 [i.e. the user doesn't have to care
 about explicitly saving/restoring data files and session state anymore,
 while the programmer is relieved from
 explicitly browsing file systems and checking file formats],
* consistent distribution of objects
 [you don't have to manually manage stale links as with the WWW,
 or adequacy of several versions of a "same" software product],
* fine-grained programming
 [you don't have to rewrite the whole of Word
 to support your national language,
 or re-buy all of a business administration tool
 to support the new tax computation method and declaration form],
* decoupled user interface
 [the interface is produced separately from the actual algorithms,
 so that it is fairly trivial to replace a Graphical UI
 by a Voice UI (for the blind or for screenless portable computers),
 or a tactile UI (for the blind),
 or eye-blinking UI (for paralyzed persons,
 or silent interface in a submarine),
 or a network interface (for remote users), etc].
All in all, this makes you
the master of the computer rather than its slave,
and frees you from the status of hostage of your current
software supplier as is the case currently
[I know lots of people in various business who are bound
to stay with the same lame software,
because they can't upgrade it,
and they can't change to another, incompatible, supplier]


The philosophical idea is that computers are a way to exchange
and manipulate information;
and information basically has two aspects: Liberty, and Security.
   Security is being able to to know what you have,
and be sure that you won't be suddenly deprived from it,
so you can build upon it. It is being sure that contracts
that were agreed upon will be fulfilled.
   Liberty is being able, in the limit of previously agreed contracts,
to do what you want, to be able to devise new contracts with exactly
what you want inside, and never be forced to sign more than you would.
   Systems that don't allow you to express the contract you want,
by not letting you write what you like and agree with whom you like
(in the limits defined by former contracts) are stupid unfree systems.
   Systems that do allow you to express the contract you want,
but have no way to enforce it, or have "exception" clauses
that at times will void your rights, are ineffective unsecure systems.
   Systems that enforce contracts that you don't want,
or add clauses that you object to are fascist unfree systems.
   Well, Tunes tries to be a free, secure system:
people define arbitrary object specifications (contracts),
thanks to a maximally expressive language;
as guarantees to these contracts, proofs are given
that will be checked by the system.
   Of course, if a proof was not given to you,
you can always run the program by explicitly admitting part of the proof.
But then you will have knowingly taken a risk,
and chosen to lessen your security;
at no time may the system do that silently in your back.
YOU control what you have, you know what you are given,
and are free to refuse a contract without sufficient warrantee.

   I hope I have been understandable.
Tell me if anything wasn't clear.
I'd really not like my ideas to be ignored
just because I can't explain them well enough...

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