Universal Typesystem

David Manifold dem@tunes.org
Tue, 19 May 1998 04:16:24 +0000 (GMT)

The core of TUNES could be called a "universal type-system."  Such a UTS
needs to:  Fully and precisely specify all details, with universal
semantics for abstraction, reification, and evaluation. 

Full specification is the equivalent of full source, so it allows
everything to be changed.  (If you can't change it directly, just copy it
over and change it somewhere else)

Universal semantics for evaluation allows anything to be equally
manipulated by the user, programmer, and the computer.  (Performing an
action is the same no matter what decided to perform it)

Universal semantics for abstraction/reification allows the typesystem to
describe every part of the system at every level (this brings your
uniformity, modularity, security, etc.)

The universal typesystem describes hardware in exact detail, and is
reflective, so it can port itself to any platform defined in the UTS.
(which makes it universal between computing systems, not just throughout a
single system)

The UTS is fundamentally based on logic, set theory, and mathematics.
Evaluation is translation from one theory (type) to another.  Proof is
following the path to validate the theory.  Getting the definition of
something is retrieving the proof, so proving something is the same thing
as adding it to the system.  Making a hypothesis is creating an object
that is not yet defined: completing the definition is finishing the proof,
which can be done by either the user or the computer or a combination of
both.  Something else that can be done is starting from defined terms, and
trying to figure out new meaning.  The computer or the user can do this.
Writing programs or constructing models is one example of creating new
meaning from old.

David Manifold <dem@tunes.org>