# Vision
Topos is an autodiff compiler stack. Record a graph, inspect
it, differentiate it, compile it, emit it. The spec is an immutable
value and the state is yours. The network never moves; a training
step is a pure data transform of caller-owned parameters.
The goal is a complete compiler whose first-principles design makes
it the easiest place to build the next thing. Better a few strict
rules than lots of features: that is how the next idea stays easy.
Once the graph is written, its sizes do not change.
That means three commitments:
- **The whole modern ML-compiler stack, small enough to read.**
One spec, a short list of named interpretations of it. Every
stage is visible and printable, none of it magic.
- **Every result provable.** The plain interpreter is the
executable spec; anything faster must match it, bit for bit by
default. A claim is one assert away from proof.
- **Built for learning, research, and production.** New ideas
plug in at named seams, with the oracle as ground truth. The
core stays closed and simple on purpose. Completeness is the
point: the stack aims at the whole compiler.
A typical compiler rewrites the program until it becomes something
that can run. Topos does not. The tape is written once; everything
after it is a named way of reading the same spec. That list is the
compiler — small enough to read because there is nothing else.
- Recording writes the tape and infers every shape at the
expression that records it. Sealing freezes that as the spec.
- The interpreter runs it. Those bits are the truth.
- Reverse mode is the same scan backward. The same derivative
rules can also record themselves as ordinary nodes, so compiled
training is a forward plan over that extra tape — fusion and
liveness then apply to the chain rule itself.
- A plan is a schedule of what to run, what to keep, and what to
free. It is derived from the spec and holds no state.
- Fusion is an offer a run may elect, never a rewrite of the tape.
- Emission writes the plan as text for an industrial backend. It
is a sibling of `describe`, not a second compiler.
That list is also where new work lands. A new element type, a new
fusion, a new backend, a new emission target, a new AD mode —
each plugs in at a named seam and is proven against the
interpreter. The idea does not need a fork, and a hand-rolled
equivalent has the same standing as a built-in.
Adoption may follow; it is never chased. No benchmark races, no
coverage races, no plugin bazaar.
## The rules
Five rules, one axis each: what a program means, what may be
read, what is true, how a faster form earns its spelling, what
the core owns.
1. **The tape is the spec.** Recording writes it, sealing fixes
it. Everything downstream — derivatives, plans, fusions,
backends, emission — is a derived artifact: free to change the
spelling, forbidden to change the meaning. Shapes are static
and tapes are cheap — one tape per shape bucket, re-record
rather than generalize. A plan holds no state, so it survives
every training step and every reopen.
2. **Say what you want to read.** Observability is declared —
roots and observes — never inferred, and a read outside the
declaration fails loudly. The declaration is the license every
optimization runs on: the observed must survive any rewrite;
the unobserved is fair game to fuse away.
3. **The interpreter's bits are the truth.** The plain interpreter
is the executable spec, and every plan, backend, and emitted
module must reproduce its bits by default. Seeded runs replay
exactly; anything that reorders float math is a labeled option,
never a silent one.
4. **Composition is the default.** A fused or native form buys
its way in with a measured reason — float behavior or real
cost. The primitives compose; specialized spelling is earned.
5. **The core is enough; facades prove it.** The core owns
exactly what the crate exists to do. Every facade — layers,
optimizers, losses — composes through the public surface
alone, so a hand-rolled equivalent behaves identically and
each facade stands as proof that the primitives suffice.
## Principles
Constraints the vision names without arguing. One file per
principle; the type names in each "Spelled today" section may
rot, the rest must not.
- [Recorded reverse mode](principles/recorded-reverse.md)
- [Spec and state](principles/spec-and-state.md)
- [Names](principles/names.md)
- [What earns an instruction](principles/vocabulary.md)
- [The element is the seam](principles/element.md)
- [Observability is a license](principles/observability.md)