I'm on the right track.

[David Manifold]

I was reading about NuPrl and found something I just had to comment on.

(From http://simon.cs.cornell.edu/Info/Projects/NuPrl/book/node10.html:)
"Proofs can be thought of as finite trees, where each node corresponds to
the application of a logical rule. A proof can be read to the desired
level of detail by descending into subtrees whose structure is interesting
and passing over others."

In TUNES, adding an object to the system is the same as "proving" it.
Therefore, using TUNES is equivalent to NuPrl's "proof editing":  You
browse the tree of your system to a desired level of detail (think of
running an app in a current system), and edit something (think of
performing a command in some application).  

Now, there are different levels of proving something, which just means
that objects of different trust will be found in different places in the
system.

David Manifold <dem@tunes.org>