Tunes

[Francois-Rene Rideau]

Dear M. Stallman,
   I'm a french student at the Ecole Normale Superieure,
and have undertaken my own free software project for a new OS, Tunes,
about which I would have liked to ask you your opinion.
   I understand you must be *very* busy doing your wonderful work
about the FSF, GNU, Emacs, Guile, etc.
Hence, feel free not to answer me if you don't have time.
   However, I would appreciate a short reply to tell me
that you want me not to bother you anymore, if that's the case.
Even if you're not personally interested,
perhaps you can forward this message to people who will be,
or get me in touch with people who can help me be more useful.



I conceive Tunes as the next generation of free OS after Linux and HURD,
which was a first generation implemented in the most expedient way,
so as to have any free software platform at all to begin with.
   While GNU focused on Unix compatibility, so as to allow a seamless
transition from a corporate racket into a free software market,
Tunes focuses on providing cleaner abstractions
to free software developers, so as to reduce the overhead of
writing free software, and hence making a richer, more fluid, market.

The basic idea is that existing software isn't reliable per se,
because development tools and platforms are basically unsecure.
POSIX, for instance, is a huge piece of software,
for which providing formal semantics is hardly imaginable,
not to talk about proving an implementation correct,
or using the proven semantics.
Hence, trying to prove correct software that relies upon such
unsecure basis is not very useful.
   Also, the very low-level nature of the C programming language
and the standard C libraries make it very hard to prove any software
written with those. Moreover, because these languages cannot
express security constraints, correctness proof in the context
of arbitrarily buggy low-level processes running around is useless.
You can't have, e.g. persistent data that will reliably survive
powerfailures, not to talk about other programs that might clobber
your data without anyway for you to prevent or even detect it.
   99.9% of programming is spent rewriting new versions of old algorithms,
with a new low-level interface to some implementation,
lots of stubborn low-level I/O interface that's
either unsecure or bloated with error checking,
either unfriendly or bloated with user interface code,
either unextensible or bloated with yet another extension language, etc.
Rewriting the old stuff is good if to correct bugs,
or for students to learn by doing.
But that's clearly not the kind of constant rewrite being done.

Tunes wants to end that huge programming nonsense.
It will provide a reflective functional language
with higher-order modules and functors,
and a very expressive type system that can be used
for program specification and proof
[Something between Scheme, Coq, Clean, and Objective CAML].
   Proven-correct low-level programming will be made possible
thanks to families of modularized low-level implementations
being reflected, specified, and proven, into the high-level language.
Tunes will allow the user to completely control the assumptions one
make about the system, whereas existing OS fuck you from behind
by silently making false assumptions every now and then.
   Actually, the only unproven part of the system could be the
hardware specification (well, if hardware was designed using
formal methods, we could prove its design, but still,
we'd have to trust the manufacturing plant, etc),
and the proof checker itself.
However, those parts being freely available and of relatively small size,
one will be able to have a most solid trust in them after they've been
reviewed long enough by all the proficient people in the world,
who will undoubtly use it and support it.

The Tunes language will eventually be much more efficient
than existing implemented languages,
because it will stress on separating design and implementation,
and allowing reflective control of code-generation
so as to compile proven-correct high-level code
into blazing fast low-level code.
   In current low-level programming languages,
where the compiler output is essentially a straightforward translation
of the source code, up to some local optimizations,
the design directly maps the implementation. Hence you must make
a compromise between abstraction, maintainability, security, etc,
and efficiency, support of legacy code and libraries.
   On the contrary, Tunes source will be made of
well-separated high-level objects, that you *can* specify and prove correct,
but that you can have the compiler implement is a completely ad-hoc way,
as long as you can prove that the compiling tactic preserved the
program's observable semantics.
   Dynamic partial evaluation and invalidation will be used to
provide excellent performance in a dynamic system,
and will encompass code generation, caching, etc.
For instance, it will inline all dispatches and local calls,
so that "sending a message"
(I hate that OO terminology -- can't people just say "applying a function" ?)
to an object in a foreign module that will increment a counter
might be implemented as just "incl %eax", etc.
   Protection domains need not be implemented at all,
as a strongly typed language with first-class environment
can logically implement infinitely better security than any
stubborn runtime protection domain. However, no one is prevented
from implementing such domains for such purpose like emulating old OSes.


I might say a lot more, but time is lacking to me today.
My main problems are about organizing my time,
and having my works recognized by the community,
at least enough so I can focus on it without worrying about
my financial disaster.
   If you've made it to there, I already thank you.
Any feedback welcome. Any help appreciated.


   Regards,
and thanks again, again, and again, for your *wonderful* work
at promoting free software in the world.
If you didn't exist, God ought to invent you (if he existed).


PS: the WWW homepage for Tunes is
	http://www.eleves.ens.fr:8080/home/rideau/Tunes/

The mailing lists are
	tunes@ens.fr
	tunes-lll@ens.fr
[LLL stands for "Low-Level Language", i.e. implementation]
To which one subscribes through listserv@ens.fr

--    ,                                         ,           _ v    ~  ^  --
-- Fare -- rideau@clipper.ens.fr -- Francois-Rene Rideau -- +)ang-Vu Ban --
--                                      '                   / .          --
Join the TUNES project for a computing system based on computing freedom !
                 TUNES is a Useful, Not Expedient System
WWW page at URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"