formally verifiablecompiles to bare metalwrite in space, deploy on earththere is not one universecompile in space, deploy in spacemany universes, in present timewrite in space, deploy in spaceproven safe at compile timecompile in space, deploy on earthmemory safety without overheadcertification readymachine code, any platform
Space is a formally verifiable programming language. Proven safe at compile time. Compiles to machine code.
Space code compiles to SPARK, a safety-critical language used in aerospace and mission-critical industries. GNATprove proves your program is free of entire classes of bugs. Then GNAT, a production compiler with 30 years of optimization, outputs machine code for Linux, macOS, Windows, or bare metal.
Some spacecraft run Forth — processors like the RTX2010 execute it directly. Space is designed for similar capability: a verified compiler small enough for embedded hardware. Write in Space, compile in space.
Other languages have memory pools, arenas, regions, actors. These are allocation strategies or isolation mechanisms.
Space has universes: isolated memory regions with their own stack, their own discipline, and their own lifetime semantics.
1024 linear create-universe as scratch
\ This is a self-contained world
\ Nothing escapes. Nothing leaks in.
end-universe scratch
A universe isn't a memory pool. It's a bounded context of meaning. Pointers inside have significance. Outside, those same bits are meaningless — addresses into void.
No other language treats isolation as a semantic primitive.
Linear types exist in Rust, Clean, Linear Haskell, ATS. But in all these systems, you track individual values.
Space tracks whole universes. A linear universe self-destructs when its obligations are fulfilled — when the stack empties.
1024 linear create-universe as temp
42 push
pop \ obligation fulfilled
end-universe \ universe already gone — this acknowledges it
No explicit free. No destructor call. No reference count hitting zero. Completion itself is the cleanup.
The end-universe doesn't destroy anything. It witnesses what has already happened.
No other language has self-destructing execution contexts.
Substructural type systems (linear, affine, relevant, ordered) are typically applied to individual values.
Space applies disciplines to universes:
| Discipline | Copy | Drop | Universe Behavior |
|---|---|---|---|
| Unrestricted | Yes | Yes | Immortal — never destroyed |
| Affine | No | Yes | Explicit release required |
| Linear | No | No | Self-destructs when empty |
This is coarser-grained but simpler to reason about. You don't track whether each variable is linear. You track whether the whole context is linear.
No other language applies substructural disciplines at the container level.
Every language with pointers gives you addresses. When you traverse a data structure, you hold a pointer to your current position. That pointer can escape. It can be stored. It can outlive its validity.
Space has warps: you enter a data structure and navigate, but you never hold a pointer to where you are.
ptr warp-into as w
w warp-fetch \ read current position
1 w warp-advance \ move forward
w warp-follow \ follow a reference
end-warp w \ must close — warp is linear
Inside a warp you can see the current value, move to adjacent positions, follow references. But you cannot extract your current address. The position exists only within the warp context.
This is traversal without mapping. You can explore a data structure without creating a map of where you've been.
No other language separates navigation from addressing.
Text representations in existing languages:
| Language | Unit | Random Access |
|---|---|---|
| C | bytes | O(1) |
| Java | UTF-16 code units | O(1) |
| Python 3 | code points | O(1) |
| Rust | bytes | O(n) for chars |
| Swift | grapheme clusters | O(n) |
| Space | grapheme clusters | O(1) |
Space stores grapheme clusters — what users perceive as characters — with O(1) random access.
A family emoji (👨👩👧👦) is 25 bytes in UTF-8, 11 UTF-16 code units, 7 code points — but 1 grapheme. Space indexes by graphemes. Position 0 is the whole family emoji.
No other systems language has O(1) grapheme-indexed text.
Other verified languages (SPARK, Dafny, F*) are powerful languages with proofs bolted on.
Space inverts this: it's a simple language where verification falls out naturally.
The design question wasn't "how do we verify this feature?" It was "what features can we have while keeping verification tractable?"
The constraints aren't limitations. They're the architecture.
Individual features have partial analogues elsewhere:
| Feature | Elsewhere | In Space |
|---|---|---|
| Self-destructing contexts | None | Linear universes |
| Address-free navigation | None | Warps |
| Grapheme text | Swift (O(n)) | O(1) random access |
| Linear types | Rust, Clean | At container level |
| Isolation | Erlang actors | Universes with disciplines |
| Concatenative | Forth, Factor, PostScript | With universe-scoped stacks |
| Verification | SPARK, Dafny | Designed so proofs fall out |
The combination is new. Each piece reinforces the others:
Space demonstrates that:
The unique features aren't arbitrary. They're answers to the question: what's the simplest possible system that can be verified, parallel, Unicode-correct, and suitable for safety-critical use?