on obligations, boundaries, and the nature of ownership
Space is a concatenative systems language where memory lives in isolated universes that self-destruct when their obligations are fulfilled. Values carry disciplines — unrestricted, affine, or linear — that govern whether they can be copied, dropped, or must be consumed. Pointers cannot escape their universe. Safety is not enforced at runtime; it is proven at compile time.
Most languages ask: who frees this memory? Space asks: what must be true before this memory can cease to exist?
A linear universe doesn't need someone to destroy it. It destroys itself when its obligations are fulfilled — when every value has been consumed, when the stack is empty, when there is nothing left to do.
1024 linear create-universe as scratch
42 push
pop \ obligation fulfilled
end-universe \ universe already gone
The end-universe doesn't destroy anything. It acknowledges what has already happened.
A universe is not just a memory region. It is a context of meaning.
Inside a universe, pointers have significance. They refer to locations, carry obligations, represent relationships. Outside the universe, those same bit patterns are meaningless — addresses into void.
This is why pointers cannot escape. It's not merely a safety rule enforced by the compiler. It reflects a deeper truth: meaning is contextual. A pointer's significance depends on the universe that gives it meaning. Remove the context, and you remove the meaning.
The map is not the territory — but without the territory, the map is nothing.
Each universe operates under a discipline — a set of rules governing how values behave:
These aren't arbitrary restrictions. They're different ontologies — different answers to the question what kind of thing is a value?
Numbers are unrestricted because the number 42 doesn't get "used up" when you read it. File handles are affine because there's only one underlying resource, and you can choose to abandon it. Linear values are promises that must be kept.
When you borrow a pointer from another universe, you're not taking ownership. You're being granted temporary access under strict terms: you may look, but you may not keep.
The borrowed pointer is affine — it must be returned (dropped) to end the borrow. This isn't bureaucracy. It's the formal expression of a social contract: I trust you with access to my internal state, but that trust has a scope.
borrow-pointer \ trust extended fetch-borrowed \ access granted drop-pointer \ trust returned
The source universe cannot self-destruct while borrows are active. Your temporary access creates a dependency — a relationship that must be resolved before either party can move on.
A warp is stranger than a borrow. When you warp into a data structure, you enter it — but you never hold a pointer to where you are.
Consider the difference: a borrowed pointer gives you a location. A warp gives you a perspective. You can see what's at the current position, move to adjacent positions, follow references — but you never learn the addresses involved.
This matters because internal pointers are the most dangerous kind. They create implicit dependencies, hidden relationships that survive beyond their intended scope. Warps eliminate this possibility by design. You can traverse without mapping. Navigate without recording.
The tourist sees the city. The cartographer owns it. Sometimes you only need to be a tourist.
Space has many rules. Pointers can't escape. Linear values must be consumed. Borrows must end. Warps must close.
These constraints might seem oppressive. But consider what they enable:
Each constraint eliminates a class of errors. And more importantly, each constraint eliminates the possibility of those errors. You don't need to think about use-after-free because the type system makes it unrepresentable.
This is freedom through structure. Not the freedom to do anything, but the freedom from having to worry about everything.
Space is implemented in F*, a language where types can express properties and the compiler checks proofs. This isn't testing. Testing shows that something worked in specific cases. Proof shows that something works in all cases.
When the specification says "pointers never escape their universe," that's not an aspiration. It's a theorem. The F* compiler has mechanically verified that the property holds for every possible program. Not most programs. Every program.
This changes the nature of trust. You don't trust that the developers tested thoroughly. You don't trust that the documentation is accurate. You trust mathematics.
Why Space? Why Universe? Why Warp?
Because the metaphor is apt. Universes in physics are causally isolated — events in one cannot affect events in another. Space's universes are similarly isolated — memory in one cannot corrupt memory in another.
Warps in physics allow faster-than-light travel by bending space rather than moving through it. Space's warps allow traversal of data structures without exposing the paths traveled.
The cosmic scale isn't grandiosity. It's precision. These concepts operate at the foundational level of the language, shaping everything built on top of them. Foundations deserve foundational names.
Space is not a simple language. It has universes, disciplines, obligations, borrowing, warps, and more.
But consider what it doesn't have:
The complexity of the language absorbs the complexity that would otherwise live in your program. Every rule Space enforces is a bug you don't have to prevent, a test you don't have to write, a vulnerability you don't have to patch.
Simple systems have complex failure modes. Complex systems can have simple failure modes — or none at all.
There's something almost meditative about linear universes. You create one, perform your work, consume every value, and it vanishes. Nothing is left behind. No cleanup. No residue. No trace.
This is how computation should feel. Not accumulation — transformation. Not ownership — stewardship. You receive values, process them, pass them on. When you're done, you're done.
The empty stack is not emptiness. It's completion.