stone

A minimalist programming language where the only primitive type is set.

Stone uses set theory to express computation. Numbers are Von Neumann ordinals, booleans are sets, pairs are Kuratowski encodings, and conditionals emerge from set comprehensions.

Published at SIGTBD 2026 (MIT CSAIL)

Read the paper (PDF)

One Type to rule them all, One Type to find them, One Type to bring them all, and in the emptiness bind them.

—J.R.R. Tolkien

Nothing is certain, but everything is set in stone.

—Zen kōan

Install

cargo install --path .

This puts stone on your PATH. Then:

stone                           # REPL
stone examples/fibonacci.stone  # run a file
stone --theme zen               # REPL with zen display

The Language

Everything is a Set

Concept	Encoding
false	{} (empty set)
true	{{}} (set containing empty set)
Natural n	Von Neumann: 0={}, 1={{}}, 2={{},{{}}}, ...
Pair (a,b)	Kuratowski: {{a},{a,b}}

Syntax

-- This is a comment

-- Binding
x := 42

-- Constants
true  false  empty

-- Set literals and comprehensions
{1, 2, 3}
{x + 1 : x in 5}            -- map: {1, 2, 3, 4, 5}
{x in 10 : x in 5}          -- filter: {0, 1, 2, 3, 4}
{x * x : x in 4, x in 2}    -- map+filter: {0, 1}

-- Set operations
A \/ B                        -- union
A /\ B                        -- intersection
A \ B                         -- difference

-- Arithmetic (on Von Neumann naturals)
3 + 4                         -- 7
5 - 3                         -- 2 (truncated: 3 - 5 = 0)
3 * 4                         -- 12
7 / 3                         -- 2 (integer division)

-- Unary operations
!false                        -- true (boolean negation)
|{1, 2, 3}|                  -- 3 (cardinality)
Union{{1}, {2, 3}}           -- {1, 2, 3} (big union)
Intersection{{1, 2}, {2, 3}} -- {2} (big intersection)
Power({1, 2})                -- {{}, {1}, {2}, {1, 2}} (power set)

-- Comparisons (return true or false)
A == B    A != B
x in S    x !in S
A <= B    A < B               -- subset, proper subset

-- Assertions
assert 3 + 4 == 7

-- Functions
fn x. x + 1                  -- lambda
f(3)                          -- application
fn(x, y). x + y              -- pair destructuring

Conditionals

There is no if/then/else. Instead, selection emerges from set comprehensions. The standard library provides cond:

cond := fn b. fn x. fn y. Union{x : _ in b} \/ Union{y : _ in !b}

Usage: cond(condition)(then_value)(else_value)

cond(true)(1)(2)   -- 1
cond(false)(1)(2)  -- 2

Recursion

Bindings are implicitly recursive:

fact := fn n. cond(n == 0)(1)(n * fact(pred(n)))
fact(5)   -- 120

Standard Library

The prelude defines five functions:

Name	Description
cond	cond(b)(x)(y) -- conditional selection
succ	succ(n) = n + 1
pred	pred(n) = n - 1
fst	fst((a,b)) = a
snd	snd((a,b)) = b

Pretty-Printing

The REPL recognizes and displays:

• Von Neumann naturals: {{}, {{}}} -> 2
• Kuratowski pairs: {{a},{a,b}} -> (a, b)
• Empty set / zero / false: {} -> 0

Examples

Boolean logic:

false \/ true    -- 1 (OR)
true /\ false    -- 0 (AND)
!false           -- 1 (NOT)

Von Neumann ordering (m < n iff m in n):

2 in 5           -- 1 (2 < 5)
5 in 3           -- 0 (5 < 3 is false)

Fibonacci:

fib := fn n. cond(n == 0)(0)(cond(n == 1)(1)(fib(n - 1) + fib(n - 2)))
fib(7)           -- 13

Set comprehensions:

{x * x : x in 6}             -- {0, 1, 4, 9, 16, 25}
{x in 10 : x in 5}           -- {0, 1, 2, 3, 4} (filter: x < 5)

Pairs and projections:

p := (3, 7)
fst(p)           -- 3
snd(p)           -- 7

Operator Precedence (lowest -> highest)

Prec	Operators	Assoc
1	:=	right
2	== != in !in <= <	none
3	\/	left
4	/\	left
5	\	left
6	~> ?>	left
7	+ -	left
8	* /	left
9	! Union Intersection Power |.|	prefix
10	f(x)	left

Symbol Themes

The default syntax uses typable ASCII. Alternative themes preprocess Unicode symbols before parsing.

stone --theme mathematical file.stone  # Unicode math: λ, ∈, ∪, ∩, ...
stone --theme zen file.stone           # Contemplative: ▸, ☯, ●, ○, ⋔, ...

Files containing Unicode symbols are auto-detected.

Semantic	Default	Mathematical	Zen
lambda	fn	λ	▸
equality	==	==	☯
membership	in	∈	∈
union	\/	∪	∪
intersection	/\	∩	∩
difference	\	\	\
negation	!	¬	¬
multiply	*	×	×
divide	/	÷	÷
big union	Union	⊔	⊔
big intersection	Intersection	⊓	⊓
power set	Power	℘	❊
true	true	⊤	●
false	false	⊥	○
empty set	empty	∅	○
not equal	!=	≠	≠
not member	!in	∉	∉
subset	<=	⊆	⊆
proper subset	<	⊂	⊂
assert	assert	assert	◆
ripple	~>	~>	≋
sift	?>	?>	▽
conditional	cond	φ	⋔
successor	succ	σ	↑
predecessor	pred	ρ	↓
projection 1	fst	π₁	⊏
projection 2	snd	π₂	⊐
zero (display)	0	∅	○
one (display)	1	1	●

License

MIT