How to do Tunes

[dufrp@oricom.ca]

> what?!?  why low-level stuff?  why products designed by conservative
> thinkers?  'favorite language'?!?  you're addicted to the old system.
> we're here to make a new system.

But this 'new' system we want is just a bunch of already existing
stuff. When we say we want a persistent. distributed system we are
almost saying that we want to do a port of Grasshopper OS (for 
alpha processor) to the x86 family. Or that we want to add
distributed aspects to the L4 Linux OS. Maybe using the pc 
exokernel-based OS that is now a 50Mb monster.

When we say we want a system that replace hardware protection by
proved-correct code, we mainly say we want a slightly modified
version of Coq proof system with added reflectives abilities.
Maybe some reflective system like Maciste.

> >If you think you know how the internals of a Tunes-like system
> >could work, I suggest you take a month to try to write a 20 pages
> >paper to describe it.
> for now, i don't believe that that is possible.  i've discussed earlier
> how a full tunes system would be capable of ontological relativisation,
> giving itself new meaning for every context.  this property alone means
> that no definition is complete for tunes, since it will not suffice for
> millions of contexts which could be constructed from within tunes

I don't buy that. A programming language too can become a million
things depending of the use you do of it. That's why no one can
write a paper describing a programming language. :-)
One could say that it is different when you can change the language
by metaprogramming. But I am in the process of reading about such
a language (Agora).

> in
> addition, how do you explain to the average person what a system is
> which has no true data encapsulation?  it's like saying that nothing
> means anything, except to the system as a whole.  people just don't
> explicitly think that way on the average.
I can't think without data encapsulation. I can accept that
YOUR system is like that. But I doubt it apply to Tunes.
It is very likely that Tunes will be a single-address space OS.
As I see it I will program with a 'traditionnal' programming
language under a Tunes OS, except Tunes will require some
'specifications' and make sure my code respect it. This part of
Tunes still look magical to me. I know formal methods have been
used to proof parts of OS wrong or good. But when I tried to
read about formal methods, I seemed to enter a world in the
clouds that seems to have no relation with our ground world.