Yet another overly simple explanation of Tunes

[William Tanksley]

David Manifold wrote:

> When I read this, I wonder how it can make any sense to anybody.  Tell me
> if it makes sense to you.  Anyway, it probably isn't anything new.

It makes sense to me --- but ONLY because I've been following Tunes for a LONG
time and do quite well at computability theory.  And even for me, even though
it makes sense, it's gibberish.

You asked for a flame, right?  ;-)

I'll try to be more serious now.  Sometimes.  :-)

> The entire system can be treated as one big expression.
> In fact, this big expression could be written as a string.

> Anything at all that can be done in the system comes down to an edit on
> the expression.  (Including programming, word processing, internet, etc)

This isn't an explanation, it's a model.  And furthermore, it's a model that's
more complicated than the original system.

> The expression is always being evaluated.

And furthermore, it's a bad model --- that's not physically possible, nor is it
correctly specified.  Here's why.

A mathematical expression does not need to be evaluated; it just IS.  Anytime
you talk about evaluating something, you are thinking of taking a non-zero
amount of time to cover the expression and find its result.  Thus, when you say
"is always being evaluated" you fail to answer the three most basic questions:
can two parts be evaluated at the same time?  Is the giant expression always
consistant?

And the last question: why should it matter if the giant expression was always
being evaluated?  What happens when I turn my computer off?  Doesn't that
violate the statement "the expression is always being evaluated"?

Thus, I've uncovered two problems with the statement: first, it doesn't say
anything about the evaluation itself, and second, it doesn't say anything about
'always'.

> The reason it is always
> evaluating is that each object has at least one element in its
> specification, that of "existing".

Non sequitur.  Big-time.  (What's the Latin word for "big-time"?  "Tempus
gravis"?)

> So the existence of the system is
> constantly evaluating, as long as the system exists.

I think that my acceptance of this sentance is conditioned on my acceptance of
the previous one (the non-sequitur), so I won't comment.

> Since the system is constantly evaluating, an edit on the expression will
> cause changes to take place immediately.  Any changes that are not to take
> place immediately (or subexpressions that are not to be evaluated yet)
> will simply be specified to not evaluate yet.  The constraint to not
> evaluate will still be constantly evaluated.  (Until it is changed, at
> which time the expression it is referring to gets evaluated.)

Aside from your talking about "constantly evaluated", which we have already
shown to be a false model, this is good.  In fact, I would go so far as to say
that this is a tautology --- you're saying that the system is an expression,
and that therefore any changes in the expression model changes in the system.

I agree, but I don't see any use.

> I would appreciate comments on this.. I can't make any progress on the
> system unless there is a discussion of my posts and the ideas get refined
> so that they are understandable.  Thank you very much.

I'm happy with your work so far --- I think that your study of tree-structured
proof systems will be very useful.  I would suggest that you look at: Design By
Contract (www.eiffel.com), Linear Logic (I don't remember the www location, but
the paper's subtitle is "The Forth Shall be First"), literate programming
(Knuth --- need I say more?), and Abstract State Machines.

Literate programming is included in that list because learning how to program
literately allows you, the system designer, to think outside the boundaries of
your programming language as far as code order goes.  I don't think that code
should have to be written in a literate programming language to be useful under
Tunes --- although I do think that a literate version of Forth would be
amazingly useful.

Design By Contract is useful.  Period.  It's a must-read.

Linear Logic is actually covered quite well in DBC's discussion of
concurrency.  The LL web page is nice, but suffers from severe mathitis
(inflammation of math at the expense of realism).

Abstract state machines could possibly provide exactly the formal mechanism you
need to carry out your proofs, together with the formal statements of Design By
Contract and the tree structure encouraged by literate programming.

> Won't someone ask how reflection works??

I think we have a far, far more basic question: how does the most elementary
operation work?

> Does anybody have any questions about the practicality of the above model?

I have serious doubts about it.  I don't think it's a good model.

> Any specific questions about "how do I do X in Tunes"?

I don't want to do X in Tunes.  X is a horrible hack.  Even MGR is better.

I don't think the important question is "how do I do this."  I think the
important question is "how does the system know that doing this is safe for
it."  I think that's the only thing that Tunes will do better than other
systems.

> What we need is some vehement anti-tunesers to
> start flaming the list.  Maybe we should go trolling on the usenet...?

Naw, I'll act the part.  A friendly opponent is worth far more than a hostile
one, IMO.  I'm sold on what Tunes wants, even though I have my suspicions on
whether Tunes can DO it.

> David Manifold <dem@tunes.org>

-Billy