stars are born
Space didn't emerge from nothing. It synthesizes ideas from multiple traditions: the concatenative programming lineage, the linear logic tradition, and the verification movement. This page traces those threads.
← older · swipe · newer →
Polish logician Jan Łukasiewicz invented prefix notation (Polish notation) in 1924 to simplify propositional logic by eliminating parentheses. His student Charles Hamblin reversed it in 1957, creating Reverse Polish Notation (RPN).
Infix: (3 + 4) × 5 RPN: 3 4 + 5 ×
RPN maps directly to stack operations: push 3, push 4, add (leaving 7), push 5, multiply (leaving 35). No parentheses needed. No operator precedence rules. The notation is the execution order.
The Burroughs B5000 (1961) was the first commercial stack-based computer. Instead of registers, it used a hardware stack for expression evaluation. This influenced both language design and the idea that stacks could be a primary computational model, not just a call convention.
The English Electric KDF9 (1963) followed, also stack-based. These machines proved that stack architecture was viable for real computing.
Hewlett-Packard's HP 9100A (1968) brought RPN to desktop calculators. The legendary HP-35 (1972) made it portable. Engineers and scientists learned to think in stacks:
To calculate (3 + 4) × 5: 3 ENTER 4 + 5 ×
HP calculators created a generation of users comfortable with postfix notation. Many Forth programmers started on HP calculators.
Charles H. Moore developed Forth between 1968 and 1970 while working at the National Radio Astronomy Observatory. He needed to control a telescope — real-time, interactive, on minimal hardware. Existing languages were too heavy.
Moore wanted to call it "Fourth" (fourth-generation language), but the IBM 1130 he used limited filenames to five characters. "FORTH" it became.
: square ( n -- n² ) dup * ; : factorial ( n -- n! ) 1 swap 1+ 1 do i * loop ;
Forth is radically minimalist. The entire language can be understood in an afternoon. A complete Forth system fits in kilobytes. Data stack, return stack, dictionary of words, threaded interpretation — that's it.
Traditional Forth has no type system. Any value can be any type. Stack underflow, type confusion, and memory corruption are easy. Forth trusts the programmer completely. This works for small programs written by experts. It scales poorly.
Space's debt: The concatenative model, the dual-stack architecture, the philosophy of minimalism. But Space adds what Forth lacks: verified type safety.
StrongForth by Stephan Becher added static type checking to Forth. Each word declares its stack effect with types:
: squared ( i -- i ) dup * ; \ integer → integer : fetch ( a -- i ) @ ; \ address → integer
The compiler verifies that stack effects match. Type errors are caught at compile time, not runtime.
Space's debt: The idea that concatenative languages can be statically typed. But Space goes further — its types track ownership and universe membership, not just data classification.
Chuck Moore's ColorForth used color as syntax. Red words are definitions. Green words are compiled. Yellow words execute immediately. No punctuation, no keywords — just color.
square dup * ;
ColorForth was polarizing. Some found it elegant; others found it inaccessible. But it demonstrated that syntax is arbitrary — what matters is semantics.
Space's debt: The courage to rethink syntax conventions. Space uses hyphenated compound words (create-universe, end-warp) rather than Forth's terse conventions.
Factor by Slava Pestov is a modern concatenative language with a sophisticated type system, garbage collection, and a large standard library. It proves that concatenative programming can scale to large applications.
: factorial ( n -- n! )
dup 1 <= [ drop 1 ] [ dup 1 - factorial * ] if ;
Factor has quotations (anonymous functions), combinators, and a rich ecosystem. It's the most "practical" concatenative language today.
Space's debt: Proof that concatenative languages can have real type systems and support complex programs. But Factor uses garbage collection; Space uses linear types for deterministic resource management.
Joy by Manfred von Thun explored concatenative programming from a theoretical angle. Joy has no named parameters, no variables — only stack operations and quotations.
[dup *] map
Joy demonstrated the mathematical elegance of concatenative programming: programs are compositions of functions, and composition is associative.
Space's debt: The theoretical clarity that concatenative programming is fundamentally about function composition.
PostScript is a stack-based page description language. Every PDF you've ever read was rendered by a PostScript descendant. It proved that stack-based languages could succeed commercially at massive scale.
/inch {72 mul} def
2 inch 3 inch moveto
Space's debt: Validation that the concatenative model works for real applications.
Open Firmware (originally OpenBoot) put Forth in every Sun SPARC workstation, every PowerPC Mac (1994–2006), and every OLPC laptop. It became IEEE Standard 1275 in 1994.
ok boot cdrom \ boot from CD ok devalias \ show device aliases ok words \ list available commands
Open Firmware proved Forth could handle mission-critical boot sequences. When your Mac booted, Forth initialized the hardware, enumerated devices, and loaded the operating system. Millions of machines ran Forth before the OS even started.
Space's debt: Proof that Forth-family languages belong in systems programming, not just niche applications.
Jean-Yves Girard introduced linear logic in 1987. Unlike classical logic, where premises can be used any number of times, linear logic treats premises as resources that are consumed by use.
This maps directly to memory and resource management:
| Linear Logic | Programming |
|---|---|
| Use premise exactly once | Linear type: use value exactly once |
| Use premise at most once | Affine type: use or drop |
| Use premise any number of times | Unrestricted type: copy freely |
Space's debt: The entire discipline system. Unrestricted, affine, and linear directly mirror Girard's modalities.
Clean introduced uniqueness types — types that guarantee a value has no other references. Unique values can be updated in place safely, enabling functional programming with mutable state.
:: writeFile :: *File String -> *File
The asterisk marks unique types. The type system ensures they're never aliased.
Space's debt: Proof that linear/unique types enable safe mutation without garbage collection.
Rust brought ownership and borrowing to mainstream systems programming. Every value has an owner. Borrowing creates temporary references with compile-time lifetime tracking.
fn process(data: &mut Vec) { // borrowed mutably data.push(42); } // borrow ends here
Rust proved that ownership-based memory safety could be practical and performant.
Space's debt: The borrowing model. Space's borrow-pointer / drop-pointer directly mirrors Rust's borrow semantics, adapted to concatenative style.
Robin Milner's ML introduced Hindley-Milner type inference — the compiler deduces types without explicit annotations. This made strong typing practical.
fun factorial 0 = 1 | factorial n = n * factorial (n - 1)
No type annotations, but fully type-checked.
Space's debt: The expectation that a type system can be both strong and unobtrusive.
Per Martin-Löf introduced intuitionistic type theory in 1972, creating the foundation for dependent types — types that depend on values.
Vec : Type → Nat → Type Vec A 0 = Unit Vec A (S n) = A × Vec A n
The type Vec A n is "a vector of exactly n elements of type A." The length is part of the type. Try to concatenate vectors of incompatible lengths? Type error. Try to access index 5 in a 3-element vector? Type error. At compile time.
Martin-Löf's work unified logic and computation: propositions are types, proofs are programs. This Curry-Howard correspondence is why proof assistants can be programming languages.
Space's debt: The Pointer(U) type is dependently typed — the type depends on which universe U the pointer belongs to.
Coq, developed at INRIA, was the first practical proof assistant based on dependent types. Its Calculus of Inductive Constructions allows both programming and theorem proving in the same language.
Fixpoint factorial (n : nat) : nat := match n with | 0 => 1 | S n' => n * factorial n' end. Theorem factorial_positive : forall n, factorial n > 0. Proof. induction n; simpl; omega. Qed.
Coq has verified a C compiler (CompCert), the four-color theorem, and cryptographic protocols. When you verify something in Coq, it's verified.
Space's debt: Proof that dependent types can verify real software, not just mathematical theorems.
Agda is a dependently typed language that feels more like programming than proving. Unlike Coq's tactic-based proofs, Agda proofs are written as ordinary programs with holes you fill in.
data Vec (A : Set) : Nat → Set where
[] : Vec A zero
_∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
head : {A : Set} {n : Nat} → Vec A (suc n) → A
head (x ∷ xs) = x
The type of head requires a non-empty vector. Call it on an empty vector? That's a type error. The partial function problem disappears.
Space's debt: The insight that dependent types enable total functions — no runtime failures for "impossible" cases.
Idris by Edwin Brady was designed as a general-purpose programming language with dependent types, not a proof assistant that happens to compute. It has effects, IO, and compiles to efficient code.
data Vect : Nat -> Type -> Type where Nil : Vect Z a (::) : a -> Vect n a -> Vect (S n) a append : Vect n a -> Vect m a -> Vect (n + m) a append Nil ys = ys append (x :: xs) ys = x :: append xs ys
The type of append says: concatenating vectors of length n and m produces a vector of length n+m. The compiler verifies this.
Space's debt: Proof that dependent types can be practical for everyday programming, not just verification specialists.
F* combines dependent types with SMT-based automation. You write specifications; the compiler proves them using Z3.
val factorial: n:nat -> Tot (r:nat{r >= 1})
The type says: factorial takes a natural number and returns a natural number that's at least 1, and it terminates (Tot).
Space's debt: The entire verification strategy. Space is implemented in F* and inherits its proof capabilities directly.
Space, created by Danslav Slavenskoj, synthesizes these threads into something new: a concatenative language with dependent types, linear resources, and machine-checked proofs. The design was conceived in the summer of 2025 and first implemented as formally verifiable F* code on 2026-02-10.
1024 linear create-universe as scratch
42 push
borrow-pointer from parent
fetch-borrowed
drop-pointer
pop
end-universe
The stack-based execution comes from Forth. The static typing from StrongForth. The linear discipline from Girard. The borrowing from Rust. The dependent Pointer(U) types from Martin-Löf. The verification from F*.
Universes — isolated memory regions that self-destruct when their obligations are fulfilled — are Space's original contribution. They turn resource management from a programmer's burden into a type system's guarantee.
The result: systems programming without memory corruption, concurrency without data races, resource management without garbage collection. All verified by machine-checked proof before a single line of C is generated.
Every star on the timeline above lit the way here.
Space exists because of decades of work by others:
"If I have seen further, it is by standing on the shoulders of giants." — Isaac Newton
Space is not a single innovation. It's a synthesis:
| From | Space Inherits |
|---|---|
| RPN / Stack machines | Postfix notation, stack-based evaluation |
| Forth | Minimalism, extensibility, interactive development |
| StrongForth | Static typing for concatenative languages |
| Linear logic | Disciplines (unrestricted, affine, linear) |
| Rust | Borrowing, ownership-based memory safety |
| Dependent types | Universe-parameterized pointer types |
| F* | SMT-based verification, extraction to C |
The combination is novel: a concatenative language with linear types, universe isolation, and machine-checked proofs. Each piece existed before. The integration is new.