What's the idea with details? Basically, it's that just about any programming or storage model anyone uses today can represent its state fairly comfortably as a detail, without any spare features sticking out.
For example, an obvious way to represent an XML element in Detail is to state it as a pair, whose head is the tag name (an integer), and whose tail is a pair of attribute and element lists.
In general, in an object language or other typed data model, an object is a (class content) pair. For example, to represent an IEEE floating-point number in Detail, the head might be the name of the IEEE format (eg, 64-bit double), the value its encoding as an integer. Graph structure can be constructed with an identity namespace (ie, symbolic links).
A table in a relational database is a list of tuples. A complete database is a list of (name table) pairs. (This excludes integrity constraints: about which more below.)
The state of an OS, or of a process environment in an OS, or of the runtime system of a compiled language, is a core - an informal term meaning "very large, but bounded, integer." For example, a typical computer definition has a core for each disk, real memory bank, and CPU register set.
Finally, we know from the experience of Lisp that ordered pairs are a pleasant data model for functional programs. For imperative languages, Detail also does a good job with ASTs.
If all these system models sound strangely oversimplified, it's because we've ignored the most important problem from each: assuring that changes maintain the integrity of system state.
Detail is a typeless system. This does not mean it is incapable of expressing integrity; it means that it has no hardcoded definition of integrity. In other words, an integrity test in Detail is just a function with a boolean result.
For example, integrity in most systems works inductively. The system's integrity is rarely or never checked as a whole; what is checked is a step or change function which moves the system from one state to the next. For example, a change in a relational database is an update; a change in a typed imperative language is an assignment.
The problem of inductive integrity checking is thus in general
to test whether a change may invalidate some valid state. In other
words, if
I(x) is the integrity function, and
C(x) is the change function, we want to show that for every
detail x,
(!I(x) || I(C(x))). In other words, we are
evaluating a universally qualified expression.
A type checker is a specialized component that evaluates this
function for certain restricted I and
C. Detail, being typeless, cannot have any one
built-in type checker; nor is there any general theorem prover.
Rather, it has a general facility (which we will see later) for
for specifying universally qualified expressions. (A universally
qualified expression is one that if you write it out in English,
says something like "for every x, f(x) equals g(x).")
Such universal specifications can express all the usual integrity constraints, and type systems with various binding points from static to dynamic and markup-validation style. To depend on a universal specification is to depend on a formal proof. Often this is impossible to create, and often when it is possible it is not profitable. To depend on a universal specification without having created or checked a proof is to trust it.
Trust, of course, goes up to the human level - typically through the person of your friendly local sysadmin, but also via automated remote update services. Essentially, Detail is more like an OS in that it has multiple bases of trust, than a traditional language VM environment with a single such basis (type system, bytecode verifier, etc).
Both approaches have their pros and cons, and it is impossible to say which is better. Certainly both have done much good work, and if you look at OSes and VMs today, each needs the other. By definition, the single-trust system is more secure than the multiple-trust system - all other things being equal. Which of course they rarely are.
And likewise by definition, the multiple-trust approach is more expressive. It's not fighting uphill against Godel's theorem. In other words, there is no one perfect or optimal type system. There will always be programs that leave memory in a consistent, correct state, but which your verifier cannot show are correct. Whether or not a language's semantics can express such programs is irrelevant.
Unfortunately, implementing an RDBMS is not quite as simple as specifying its inductive integrity constraint!
Here is another hard problem the above analysis overlooks: mapping the abstract data model of details into real bits and bytes. As in type checking, conventional environments solve this problem with a single hardcoded runtime system.
This approach is one of the reasons Detail is unusual in the minimalism of its abstract data model, even next to other typeless languages. For example, look at the evolution of Lisp from mathematical abstraction to practical system. In theory, everything can be represented as ordered pairs. In practice, to achieve any kind of decent performance, the runtime system needs to represent an associative array as a hash table, a vector as a hard structure, etc. The result is a glorious profusion of hardcoded types.
As with type checking, Detail does not solve this problem so much as push it up a layer. Building a real system in Detail involves modeling the system's state as a detail, and then formatting it as a core - again, a large integer (or tuple of integers) which represents real system state.
For example, the logical state of a RDBMS is a list of tables; any change to this state must maintain the RDBMS's logical integrity function. The formatted state of an RDBMS might be (for example) three cores, one each for memory, disk and a CPU; executing a CPU step or I/O operation must maintain an equivalent (but of course very different) integrity constraint.
Formally specifying the requirements of this relationship does not, of course, write the code for you. It does not even, in general, allow you to build one high-level formatting tool that solves all problems. Not that it is impossible, of course, to write a program that maps an arbitrary detail to an integer and back again, or one that converts any change to the abstract detail into a change to the integer; but no one such format will be efficient for all applications.
However, using specified instead of hardcoded formatting is not without its advantages. There are quite a few practical problems that benefit from precise definitions of "binary" data integrity and semantics. The ability to separate logic from formatting is also appealing.
Note that none of the above requires Detail to support blanks. In fact, it would probably work okay with just pairs and integers.
Blanks are desirable because in a programming environment with code-data equivalence, the most comfortable paradigm for mixing code and data requires some concept of an out-of-band escape signal. This can't really be an integer, so we need another shape.
The obvious choice is three-valued logic, because the third value (ie, neither true nor false) will rarely appear in data and makes a great escape. Once you have a three-valued shape, you notice that it is useful for quite a few things beyond true, false and unknown. Thus the yin/yang/qi naming, which clearly separate blanks into two opposites and a third, but does not (for most applications) imply any further semantics.
Yes, in some contexts, blanks are a feature that does "stick out" a little. But the extent to which they clean up functional code makes them worth it.