Tunes originality (was: a few queries)

[Francois-Rene Rideau]

>: Andrew J. Blumberg

> so the essential bits i extracted from your recent message were :
> 
> 1) it would be nice to have the capability to do proofs
> 2) it would be nice to be able to harness parallel processing
> 
> as you point out, these are trivially true assertions --- but this is not a
> particularly new viewpoint, and certainly not unique to TUNES.  there are a
> fair variety of languages which permit proofs in a better way than C, and
> there's been lots of work on parallel processing.
>
> but what do you actually plan to implement with TUNES?
> what's the important intellectual advance represented by TUNES?
> what are the new ideas?
>
I'm glad you ask, for your question is very pertinent.
This is what I want to explain in my "Why a New OS" article,
that sadly still ain't finished yet.
The first part, that is more than half finished,
gives the general project philosophy.
The second part, that is still a draft,
shall tackle the technical problems.
The third part, for which only disseminated notes exist,
will counter common myths that Tunes wants to dispell.
Do not hesitate to review the notes I published
and send me some feedback.

More precisely on the technical originality of Tunes,
here is what I can say off-hand.

TUNES isn't a project to implement a voice-based interface,
or a distributed CD database,
or a partially-evaluating dynamic run-time system,
or a hard-real-time GC,
or an object interchange format,
or a proof system,
or a parallelizing compiler,
or whatever.
   It is a project to implement a frame in which all these
could be *independently* developed as modules
that would nevertheless work
seamlessly, safely, reliably, and efficiently together.
   Most people think this is impossible,
because many have tried and failed to achieve this result before.
The advance that Tunes proposes is to show them wrong,
by providing such a prototype of such a system.
   Because among the modules we want,
some (GC, distribution) are to modify implementation
of other objects without changing their semantics,
our system must be *reflective*
(objects have access to system implementation).
   Because we want reliability and safety,
the system must be able to express the semantics to be preserved,
and check for the preservation of these semantics,
hence needs to be *as expressive as any proof system can ever be*.
   Because we want theoretical computations are useless
if they do not lead to efficient actual computations,
the system must not implement reflection
through a tower of ever slower nested run-time interpreters,
but must allow reflective definition of partial evaluation techniques
to achieve great performance, while preserving the clean semantics
(no uncontrollable system-wide reflective side-effect,
as with backdoor evaluation).
   I believe that no existing project but TUNES strives toward such a goal.
If I'm wrong, *PLEASE* do help me contact people already in such a project,
so I can join them, or at least share experience with them.
Marrying well-understood proof-friendly semantics and reflection
is THE theoretical problem that Tunes tries to solve.
This is how I intend find an academic position to develop TUNES.

Note that though most of the intended techniques for Tunes already exist,
and already have been implemented separately.
But any of these isolated feature is useless:
A proof system that cannot prove actual programs,
or a reflective system without semantic preservation,
or partial evaluation without the above
won't allow people to safely contribute efficient modules.
   For instance, the Coq system can prove beautiful theorems,
about programs or about maths.
But this won't help programmers at all,
because this doesn't work in a way that you could produce
efficient real-life programs,
and it's not reflective,
so you can't modularize implementation.
   The Descartes project at MIT is the only one in the world
to bring partial evaluation in the run-time system for
a dynamic language (Scheme).
But they don't relate it to a clean approach of program proof,
and use reflection in a very ad-hoc way.
   Similarly, ABCL/R2 and C++// have tried to use promote
reflectivity as a way to control parallelism.
But they offer neither partial evaluation
(hence having costly reflection),
neither semantically-preserving reflectivity
or any kind of program proof.
   As for lesser features, voice-control, CD database,
distributed code, fancy GUIs, etc,
all these and plenty other features have been developed elsewhere.
But these could never ever interoperate,
by lack of an expressive-enough common language.
Hence, each of these sits in its corner,
using its own crippled extension language for configuration,
talking only to the crippled tools by the same author.

Some problems with funding the TUNES project, is
1) that no large commercial companies wants to see it succeed,
because by enabling safe accumulation of fine-grained software,
Tunes will increase fair competition and promote free software,
while companies currently benefit from the current unfair market
and find most of their revenues from racket-like business practices, and
2) that no academic people cares to fund it,
because they don't care about ambitious views and industrial feasability,
only specific technical points that you can write a technical article about.
the theoretical part of the project might interest them,
though no one seems to be working on something remotely like this,
as the world of formal semantics and the world of reflection
seem to be disjoint.
   I do hope nonetheless that I can find
companies supporting the free-software model
[where you pay service-prodivers for service,
not racketting editors for protection fees],
or academic laboratories open to my ambitious vision,
that would fund me.

> almost all of the traffic i've seen here on this list has been very
> speculative and laden with claims that "TUNES will incorporate winning
> feature X". . . but i haven't heard anything particularly specific about
> implementation strategies or even an formal design.  your aims seem very
> nice, but i'm curious about how you intend to win where so many others have
> lost. . .
>
There've been more specific things and implementation strategies before,
but I've got little time now that I'm working,
so I'm rather looking for another job or research position,
where Tunes could be my official occupation.
No time for code to me currently :( :( :( :( :( :( :(
As for a formal design, I'm working on it currently.
My current strategy: looking for funding...

May by being a slow contributor not prevent others
to contribute their own code/design/comments!

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