A research language for spatiotemporal composability
revl components load, hot-swap and unload inside a running system, and “unloading leaves no residue” is a compile-time guarantee, not runtime discipline. Cordis made revertible effects a discipline; revl makes them a type system.
✓ one checked front-end · six runtimes · emitted code validated by real compilers · compiler and runtime run client-side, nothing leaves the page
The idea
Three constructs are the whole story: effect pairs a mutation with its inverse, emit admits the ones that have none, and unloading is the accumulated history run backwards. The compiler refuses everything else.
Every mutation is written as an effect … undo … pair. The
runtime pushes each pair onto the component’s accumulator as it runs,
state and its rollback, recorded together, checked at compile time (G4).
Writing to a real database, sending an email: some things cannot be
undone. revl doesn’t pretend otherwise: they must be marked
emit, the service interface must declare
emission, and every crossing lands on the audited G8
boundary surface. A tool can’t claim to be harmless when its body emits.
You never write cleanup code. Unloading replays the accumulator backwards, LIFO-complete over everything the component did (G7), and teardown itself cannot register new effects, by construction (G5). Hot-swap is just unload + re-admit, and both halves are checked.
component UserCache requires db: Database provides cache: Cache {
let store = effect Map.new() undo store.drop()
provide cache {
fn put(key, value) {
effect store.insert(key, value)
undo store.remove(key)
emit db.execute(`INSERT INTO cache_log …`)
}
}
}The gate
A rejected program doesn’t get an error code, it gets a verdict: which guarantee it broke, and the why-trace, the actual derivation the checker found. Dependency cycles, provision conflicts, silent mutations: refused before any code exists.
$
Not “type error”: G3, dependency cycles are rejected at link time, and the trace shows the cycle itself, file and line for every hop.
Diagnostics are structured (code, guarantee, expected/actual, hint),
the same document over the CLI, JSON, and MCP. revl explain G4
prints what the guarantee means and how to satisfy it.
80+ refused programs in examples/rejections/ are the
checker’s executable specification, every guarantee has a program that
proves it’s enforced.
G1 – G8
Each one is a theorem from the spatiotemporal-composability paper, turned into something the compiler refuses to violate.
Every requirement is declared, undeclared access cannot be written. A component only sees what it requires.
Provision disjointness. Two providers for one key refuse to link, per realm, so multi-tenant compositions stay coherent.
Dependency cycles rejected, with the cycle itself as the why-trace, even though loading is dynamic.
Every mutation carries an inverse (undo) or admits irreversibility (emit). No silent third option.
Teardown cannot register effects. Cleanup can’t dig new holes while filling old ones.
Code outside effect forms is pure, confinement is a type-level fact, not an escape analysis.
Derived teardown is LIFO-complete over accumulated effects. Unload order is a theorem, not a convention.
The boundary surface, externs, emissions, is enumerable. revl audit prints everything that can touch the outside world.
New on the frozen core
The core is frozen; the language keeps growing on top of it. Every addition keeps the same deal: declare the inverse, or admit the crossing. All four are checkable in the playground, and the playground can now boot them live.
component Heartbeat requires log: Log {
every 30s { emit log.write("tick") }
after 5m { emit log.write("warmup done") }
}A timer is a revertible schedule, its inverse is cancellation,
derived like any teardown. Unload provably cancels; no orphaned interval
outlives its component. Under test the clock is a coeffect:
advance 35s makes the third tick an
assertable step,
never a wall-clock race.
component Cache provides cache: Store {
handoff cache: Map[Str, Str] // the state contract
let m = effect Map.new() undo m.drop()
}A hot-swap of a stateful provider used to mean a cold successor. Now the predecessor exports its declared shape and the successor accepts it, checked at admission, with shape drift refused as a why-trace. The cache stays warm across the swap.
extern emission async fn http_post(url: Str, body: Str) -> Str
= @ts { return await fetch(url, body) }
service Http { emission fn post(url: Str, body: Str) -> Str }Asynchrony is a declared property, like emission-ness: async function values, async host externs, awaited on py/ts and erased on go/rust. A sync method reaching an async extern has no in-flight window, so the gate refuses it (A1).
component Router requires kv_a: Store requires kv_b: StoreB {
let a = effect spawn TenantAWorker with { tag: "a" } undo a.dispose()
let b = effect spawn TenantBWorker with { tag: "b" } undo b.dispose()
}A spawn may narrow a child's capabilities, never widen them. Each tenant worker provably reaches only its own store, even though the router holds both: least authority per instance, enforced by G4.
Six runtimes
One front-end enforces G1–G8 and lowers to a single IR. Six emitters target six Cordis runtimes, and conformance is measured, not asserted: each tier’s output goes to that tier’s real compiler.
A Python component can require a service a Rust component provides,
different processes, no shared address space. revl run --placement
wires each seam with a generated proxy/stub pair, and a provider’s death
becomes a reactive withdrawal, not an exception.
swap UserCache --to rust: the running composition
unwinds the component’s effects, re-admits it on another runtime, and the
system never stops.
Emitted Wasm runs fib(20) = 6765 on real wasmtime. The claim is checked by running the code, not by argument.
The component manager
Components are petits bouts, little pieces, and a composition is what you get when you assemble them. Every other package manager fetches first and finds out later. truc admits every component through revl’s own gate before it joins the assembly: a piece that would break your composition is refused at assemble time, with a why-trace, not discovered at runtime, in production, by you.
$ truc add audited_database fetched · pinned in truc.lock · vendored under trucs/ $ truc assemble --check dry run, resolve + admit, nothing touched $ truc assemble resolve → admit (G2: no provider races, G4: no capability overreach) → compose ✓ every petit bout admitted $ truc ship publish, policy-gated: official = gauntlet-graded, re-verified dossier · discoverability metadata enforced
truc add only fetches and pins. Whether the
composition still holds is assemble’s job, a
separate, honest step, with --check as its dry run
and truc rm refusing to strand a dependent.
truc is itself a revl composition, its components pass through the same admission gate they run for you, in-process. The manager dogfoods the paradigm it manages.
Every verb is also revl truc <verb>, so agents
and CI reach the manager through the toolchain they already hold.
Agent-native
revl mcp serve runs the whole compiler as an
MCP server. An agent proposing a component talks to the admission gate,
not the filesystem, and a rejection comes back as a structured document the
agent can act on, not a stack trace it has to parse.
Code, guarantee, expected/actual, fix hint, every diagnostic is a document. Measured on a 30-spec benchmark against real models, iterating against the real checker.
revl mcp schema projects services to MCP tools whose
readOnlyHint / destructiveHint
come from the compiler; a tool cannot describe itself as harmless
when its body emits.
Agent code enters a running system through revl_admit
(checked against the live manifest), or through
revl_gauntlet, which grades a candidate in isolation
and returns a verdict dossier.
The verbs themselves are capabilities: an operator profile
gates which MCP verbs a session may reach, so a read-only agent
provably cannot revl_swap a running system.
component Leaky {
config { url: Str }
let pool = effect Pool.open(config.url)
}{ "code": "G4", "line": 3,
"message": "effect has no `undo` and
`Pool.open` is not pure",
"guarantee": "every mutation carries an inverse,
or admits irreversibility with `emit`",
"hint": "write `effect Pool.open(...) undo `,
or mark the call `emit`" }component Pooled {
config { url: Str }
let pool = effect Pool.open(config.url)
undo pool.close()
}{ "admissible": true,
"provisions_gained": ["pool: Pool"],
"emission_surface": "unchanged",
"teardown": "derived, LIFO, no residue" }The toolchain is the developer surface
Because effects are revertible and boundaries are enumerable, questions that are undecidable elsewhere become cheap here.
A dry run for a hot-swap: which provisions appear or withdraw, who gets diverted, teardown order, how the emission surface changes, before anything moves.
Who emits to X? What breaks if I withdraw C? Each answer says whether it’s exact or a conservative over-approximation.
An unfinished draft still type-checks; the hole becomes a reported obligation with an expected-type fill spec, and can never be admitted.
Step an activation back over its own accumulator: :back · :bisect · :inspect. Only revertible effects make time travel cheap.
A G2/G3/G4 rejection ships the derivation, not just the verdict: put → writeThrough → audit.log.
fail at step 2; assert no residue: crash-safety as a declarable, runnable assertion in the language itself.
An undo that’s wrong is worse than none. verified round-trips the inverse N randomized times on the real runtime and asserts baseline.
Right-to-erasure evidence as a compiler artifact: proof one realm unwinds to nothing while every other realm stays untouched.
An external contract becomes a typed service, and any revl service exports back to WIT. The boundary is typed in both directions.
The gauntlet proves a candidate runs correctly; quarantine proves it cannot escape while doing so, physically, in the wasm sandbox, trap-on-escape, before it touches a hosted tier.
Progressive delivery: run both generations at once, give the successor one realm slice, promote or revert on evidence: the rollback is derived, not written.
A component faults and the system repairs itself, inside declared bounds, stopping for a human exactly when it would step outside them.
The full compiler runs in your browser, and so does the runtime. Boot a composition on cordis-py, call its operations, hot-swap your own edit into the running system (state crosses via handoff), then unload and watch the no-residue proof. The playground page is itself a revl composition: it boots itself on load, and you can withdraw, reload and hot-swap the parts of the page you're standing on. Nothing you type leaves the page.
$ git clone https://github.com/inso1337/revl && cd revl
$ uv venv && uv pip install -e ".[test]"
$ python -m revl compile examples/user_cache.rvl # source → checked IR
$ python -m revl mcp serve # the compiler as an agent gate