The Worlds Interface Metaphor

First note: since written, Squeak's Croquet/TTime system has addressed most of these issues in a small way. Move them into Slate and work upwards.

Sketch

Issues

Cool thoughts


(about inference and proof)
   Both are two sides of the same problem: define specifications of
objects, and use these specifications. Combining objects requires a
formal or informal "proof" of the specifications, and finding an
object is just proving an existential specification "there exists an
object such that...".
   We won't give info for "every possible case", which is impossible,
because we want maximal power, and thus have infinitely rich systems
so "every possible case" will not fit any finite memory. Instead,
there will be some human-controlled inference system. Interesting
proofs will be cached in databases; particularly, packages come with
standard proofs and ad-hoc provers so they can be used easily. If no
proof is available, standard programmable tools are provided so the
user can try find a new proof. As TUNES evolves, more or less complex
AI programs will appear and relieve the human from doing those proofs.
Meanwhile, superusers have the "admit it" tool, too, so they need not
be good at logic to have programs run.

(about installation / build automation)
   Sure, sure. We shall provide the most simple possible installation,
with automated mutual recognition of software packages: software being
uniquely named, and coming with formal and unformal specifications, this
is a very doable task; some AI could later allow the system to run with
less explicit information. Now, if we control the software, we do not
control the hardware, and thus we cannot be sure to install fully
automatically and recognize all the hardware at the same time.
   To conclude, software installation will be automatical and programmable
(i.e. under full user control). Default installation will be secure, but
will propose the user to try less secure hardware modules, and choose the
options for modules in general.