systems programming, verified
Space is a verified systems programming language. Memory lives in isolated universes that self-destruct when their obligations are fulfilled. No garbage collector. No runtime overhead. Safety properties are machine-checked proofs — if your program compiles, entire classes of bugs (buffer overflows, use-after-free, memory leaks) are impossible by construction.
Implemented in F*. F* is a verification language developed by Microsoft Research, used to build verified cryptography and the miTLS protocol. The Space compiler is written in F* and extracted to C or WebAssembly via Karamel.
1024 linear create-universe as scratch \ 1024 cells, linear discipline
42 push
pop \ universe self-destructs here
end-universe scratch
Why this matters: Memory bugs cause ~70% of security vulnerabilities in systems software. Space eliminates them at compile time, not through runtime checks that slow down your code. You get the performance of C with the safety guarantees of a proof assistant. No garbage collector pauses. No hidden allocations. Predictable, verifiable, fast.
A universe is an isolated memory region with its own stack. Pointers cannot escape. Cross-universe access requires explicit borrowing or warping.
1024 affine create-universe as buffer
100 allocate-bytes \ allocate in buffer
\ ... work with memory ...
release-universe buffer \ explicit cleanup
Every universe has a discipline that controls how values can be used:
| Discipline | Copy | Drop | Destruction |
|---|---|---|---|
| Unrestricted | Yes | Yes | Immortal |
| Affine | No | Yes | Explicit release |
| Linear | No | No | Self-destruct when empty |
Linear universes enforce that every value is consumed exactly once. When the stack empties, the universe destroys itself.
Temporarily access memory in another universe without taking ownership:
borrow-pointer ( ptr -- borrowed ) \ start borrow fetch-borrowed ( borrowed -- val borrowed ) drop-pointer ( borrowed -- ) \ end borrow
Borrowed pointers are affine — they must be dropped to end the borrow. The source universe cannot self-destruct while borrows are active.
Navigate data structures without exposing internal pointers:
ptr warp-into as w
w warp-fetch \ read current position
1 w warp-advance \ move forward
w warp-follow \ follow a pointer
end-warp w \ must close (linear)
Warps keep internal state contained. The position never escapes to the stack.
Space is concatenative. All cells are 64-bit.
1 2 add \ 3 dup multiply \ 9 3 swap subtract \ 6
The optional Text module provides grapheme-correct string handling with O(1) random access:
define-text greeting "Hello, 世界!" greeting text-grapheme-count \ 9 (not bytes)
Simple text (ASCII) needs no index. Complex text (emoji, combining characters) builds an index at creation. Both provide O(1) access.
| Profile | Includes | Footprint |
|---|---|---|
| Embedded | Core only | ~2KB |
| Standard | Core + Text | ~35KB |
| Full | Core + Text + Unicode | ~120KB |
These are proven in F*, not just tested:
| Property | Guarantee |
|---|---|
| Universe isolation | Pointers never escape their universe |
| Discipline compliance | Linear values consumed exactly once |
| Borrow safety | Borrowed pointers don't outlive source |
| Warp containment | Internal pointers stay inside warp |
| UTF-8 validity | All text is well-formed UTF-8 |
Extension: .space Cell size: 64-bit (all platforms) Typing: Static, concatenative Verification: F* Disciplines: unrestricted | affine | linear Universes: create-universe, end-universe, release-universe Borrowing: borrow-pointer, fetch-borrowed, drop-pointer Warps: warp-into, warp-fetch, warp-advance, end-warp Stack: dup, drop, swap, over, rot, transfer-to Arithmetic: add, subtract, multiply, divide-unsigned, modulo Logic: bit-and, bit-or, bit-xor, bit-not, shift-left Comparison: equal, not-equal, less-than, greater-unsigned Control: if-true...end-if, begin-loop...end-loop, exit-word System: halt-system, emit-byte, read-byte