# revl: a language for spatiotemporal composability

**Status:** the original v1 design (2026-08-16), kept as written; the
implemented language has grown past it (realms and interception shipped in 2.0).
The guarantees table (§4) and the tiering rationale (§8) remain normative. For
the current language see docs/syntax-2.0.md and docs/stability.md.

revl is a research language that makes *dynamic composition* (loading, unloading,
and hot-swapping components in a running system) a checked property instead of a
runtime discipline. It is the language-level realization of the paradigm
formalized in [*A Programming Paradigm for Spatiotemporal Composability*](https://github.com/cordiverse/paper)
(the "Cordis paper") and implemented as a library by [Cordis](https://github.com/cordiverse/cordis).

The name is from **rev**ertib**l**e effects, the paradigm's signature construct.

---

## 1. Thesis

The Cordis paradigm rests on two runtime mechanisms:

- **Revertible effects** (temporal composability): every mutation of the shared
  environment carries an inverse the runtime tracks; unloading a component
  replays its inverses, so removal leaves no residue.
- **Reactive coeffects** (spatial composability): a component declares the
  dependencies it reads; the runtime activates it when they are provided and
  deactivates it when they are withdrawn.

The paper proves strong metatheorems about this model (recovery exactness,
withdrawal ordering, progress, confluence). But **every one of those theorems
rests on hypotheses no library can enforce**:

| Hypothesis (paper) | Library reality (Cordis/TS, cordis-py) |
|---|---|
| Confinement (Def. 48): a component writes nothing outside its context | any closure can reach a global |
| Witnessed inverses (Def. 8): the inverse actually reverts the effect | inverse is an unchecked callback |
| Declared-only access: reads go through the coeffect specification | proxy check at runtime, or nothing |
| Provision disjointness, acyclic dependencies | runtime error at best |
| Lifecycle reentrancy invariants (§4.3) | hand-hardened after the fact¹ |

¹ Empirically: DeepSeek Harness ships a patched `fiber.ts` closing three
reentrant-disposal gaps ([vendor log, mod 6](https://github.com/deepseek-ai/deepseek-harness/blob/master/vendor/README.md));
upstream has the same territory pending in
[cordiverse/cordis#39](https://github.com/cordiverse/cordis/pull/39); the same
gaps reproduced in cordis-py and were fixed in
[geohotstan/cordis-py#1](https://github.com/geohotstan/cordis-py/pull/1).

**revl's job is to move that table's right column to the left.** The analogy we
hold ourselves to: C++ had RAII as a discipline; Rust made it a type system.
Cordis has revertible effects as a discipline; revl makes them a language.
The borrow checker governs *lexical* resource scope; revl's checker governs
*dynamic component* scope.

A second motivation is forward-looking: if components are increasingly written
by AI agents (the paper's "self-evolving agent harness" scenario, now shipping
as DeepSeek Harness), then *machine-checkable safety of a generated component
before it self-deploys* matters more than syntax familiarity. revl is designed
to be the language such a harness could require its own components to pass.

## 2. Design pillars

1. **The component is the compilation unit.** Its signature (what it requires,
   what it provides) is the whole of its interface to the world.
2. **Effects are syntactically paired with inverses.** You cannot write the
   mutation without writing (or deriving) the undo. Composite teardown is
   compiler-derived, LIFO, and not expressible incorrectly.
3. **Confinement by construction.** There is no global mutable state and no
   ambient I/O. Everything a component reaches, it reaches through a declared
   capability. "Undeclared access" is a type error, not a proxy trap.
4. **The lifecycle is the calculus.** Operational semantics follow the paper's
   §4.3 rules (Reloading/Unloading transition states, divert, failure routing,
   withdrawal guard) with the known reentrancy hardening as *spec*, not patch.
5. **Don't build a runtime.** revl compiles to an existing, hardened Cordis
   runtime (tiered backends, §8). The language is the checked front-end.

### Non-goals (v0)

- Raw native code generation (see §8; the Wasm component model is our "native").
- General-purpose ergonomics: revl v0 is for writing *components*, not
  applications-at-large; the host application assembles compiled components.
- Isolation realms and interception (§3.2.3 of the paper): deferred past v0 in this design; they shipped in 2.0.
- Verifying inverse *semantic* correctness in general (undecidable); v0 checks
  presence and shape, §6 sketches the opt-in verification story.

## 3. Language tour

### 3.1 Services (coeffect interfaces)

A *service* is the typed interface behind a coeffect key, which is what the paper calls
the coeffect at key *k*.

```revl
service Database {
  fn query(sql: Str) -> List[Row]
  fn execute(sql: Str) -> Int
}

service Cache {
  fn get(key: Str) -> Opt[Str]
  fn put(key: Str, value: Str)
}
```

### 3.2 Components

A component names its requirements and provisions in its header. The body is
its *activation*: it runs when every requirement is satisfied, and everything
it does is undone (in derived, LIFO order) when it deactivates.

```revl
component PgDatabase provides db: Database {
  config { url: Str, pool_size: Int = 10 }

  let pool = effect Pool.open(config.url, config.pool_size)
             undo   pool.close()

  provide db {
    fn query(sql)   = pool.query(sql)
    fn execute(sql) = pool.execute(sql)
  }
}
```

```revl
component UserCache requires db: Database provides cache: Cache {
  let store = effect Map.new() undo store.drop()

  provide cache {
    fn get(key) = store.get(key)
    fn put(key, value) {
      effect store.insert(key, value)
      undo   store.remove(key)
      emit db.execute("INSERT INTO cache_log VALUES ($key)")   // emission, §3.5
    }
  }
}
```

Reading guide:

- `requires db: Database`: the coeffect specification. `db` is in scope in the
  body, typed as `Database`; the component cannot activate until some active
  component provides it, and is deactivated (in dependency order, per the
  paper's Theorem 63) when its provider leaves. **`db` stays readable
  throughout this component's own teardown**; the withdrawal guard is part of
  the semantics.
- `provides cache: Cache`: the provision. Installed as an effect (with a
  compiler-derived inverse that withdraws it); the checker enforces provision
  disjointness across a composition and rejects dependency cycles.
- `effect E undo U`: a revertible effect. `E` runs at activation; `U` is
  pushed onto the component's accumulator. `let x = effect ... undo ...` binds
  the acquisition; the `undo` expression may refer to it.

### 3.3 The lifecycle is implicit

There is no `activate()`/`deactivate()` to write or call. A compiled component
is a *description*; the runtime holds the fiber state machine
(`Pending → Loading → Active → Unloading`, with divert and failure edges per
the paper's Figure 2). What the language guarantees statically:

- code outside `effect` forms is pure (no observable mutation to revert);
- every mutation is inside an `effect` form and therefore accumulated;
- nothing can register an effect during teardown (there is no syntactic
  position for it: `undo` bodies type-check against a context with no effect
  capability, which is the language-level form of the `INACTIVE_EFFECT`
  hardening).

### 3.4 Iteration boundaries and asynchrony

An activation body may `await`. Every `await` and every `effect` form is an
*iteration boundary* in the paper's sense (§4.3.2): the compiled state machine
can be diverted there, reverting exactly the effects accumulated so far. This
is the compiler-lowered form of Cordis's async-generator effects: no closure
per step; one state machine per component with inverse slots in its frame.

```revl
component Migrator requires db: Database {
  let lock = effect db.execute("SELECT pg_advisory_lock(42)")
             undo   db.execute("SELECT pg_advisory_unlock(42)")
  await run_migrations(db)          // divert point: lock is reverted if we go
}
```

### 3.5 The system boundary: acquisitions vs emissions

Following the paper's §6.1, revl distinguishes what an inverse can and cannot
mean, *in the types*:

- `effect E undo U`: an **acquisition**, revertible, tracked.
- `emit E`: an **emission**: crosses the boundary (bytes sent, rows written to
  a shared table). No inverse exists; the checker *requires* the `emit` marker
  wherever a declared-`emission` operation is called, so irreversibility is
  visible at every call site. Services declare which operations are emissions:

```revl
service Database {
  fn query(sql: Str) -> List[Row]            // observation: pure w.r.t. Γ
  emission fn execute(sql: Str) -> Int       // leaves the boundary
}
```

An `emission` may declare a `compensate` clause (saga-style), which composes in
LIFO order like an inverse but is typed distinctly: the metatheory's exactness
claims apply only to acquisitions, and the types keep the two apart.

### 3.6 Foreign functions

FFI is the only door out of confinement, and it must classify itself:

```revl
extern acquire fn listen(port: Int) -> Socket undo close(socket)
extern emission fn send(sock: Socket, data: Bytes)
extern pure fn sha256(data: Bytes) -> Bytes
```

An `extern` without a classification does not compile. This is where the
honesty lives: revl cannot verify the foreign inverse, but it can force every
escape hatch to be declared, enumerable, and auditable: `revl audit` lists a
component's entire boundary surface.

## 4. Checked guarantees (the point of the language)

<!-- docgen:guarantees-design begin -->
| # | Guarantee | Checked | Paper anchor |
|---|---|---|---|
| G1 | declared access: a component reads only what it requires | compile | Def. 25 |
| G2 | provision disjointness: one provider per key (per realm) | compile (link) | Def. 43 |
| G3 | acyclic dependencies: a cycle can never activate | compile (link) | §6.5 |
| G4 | every mutation carries an inverse, or admits irreversibility with `emit` | compile | Def. 8, §6.1 |
| G5 | teardown cannot register effects | by construction | DS mod 6 / PR #39 |
| G6 | purity outside effect forms | compile | Def. 48 |
| G7 | derived LIFO teardown | by lowering | Thm. 16 |
| G8 | the boundary surface is enumerable | compile | §6.1 |
| G9 | untrusted data cannot create authority without a declared declassification | compile (taint flow) | no paper anchor; roadmap 249 |
<!-- docgen:guarantees-design end -->

"Compile (link)" means checked when a *composition* (a set of components) is
assembled: the language has a linker phase precisely so G2/G3 are static even
though loading is dynamic: a composition manifest type-checks as a whole.
Dynamically-added components re-run the link check against the running
manifest before admission: the runtime gate exists, but it is the *same
checker*, not a separate weaker one.

## 5. Type system sketch

- **Context rows.** A component body types against a row `Γ = {db: Database,
  ...}` fixed by its `requires` clause, row-typed coeffects in the sense the
  paper attributes to Koka-style rows (§6.7). There is no subsumption trickery
  in v0: exact rows, width subtyping later.
- **Effect capability as an index.** Judgments carry a mode `m ∈ {setup,
  teardown, pure}`. `effect`/`emit` forms are only well-typed in `setup` mode;
  `undo`/`compensate` bodies type in `teardown`; `provide` method bodies type
  in `setup` (they run while active and may install effects, which join the
  accumulator; the paper's coeffect-operations-are-effects synergy).
- **Purity by default.** The expression language is pure; mutation exists only
  via effect forms and service calls. This is what makes G6 a type-level fact
  rather than an escape analysis.
- **No first-class context.** The context is not a value; you cannot store,
  return, or alias it. This closes the leak the paper's §6.7 names (a
  component reaching another's context through a closure) syntactically.

Formalization plan: elaborate revl to a kernel calculus that is exactly the
paper's §4 calculus with a typed effect language in place of opaque effect
functions; the metatheorems then transfer by construction. This (not novelty
of type rules) is the research claim: *a surface language whose every
well-typed program satisfies the calculus's hypotheses*.

## 6. What remains unchecked, and the story for it

- **Semantic inverse correctness** (`U` really reverts `E`): undecidable in
  general. v0: trusted for externs, derived (hence correct) for compositions of
  checked primitives. v1 sketch: an opt-in `verified` marker for effects over
  datatypes with algebraic undo laws (insert/remove on maps, counters), checked
  by property tests generated from the effect signature; `tests/paper/` in
  cordis-py shows the shape.
- **Independence/commutativity of keys** (paper Def. 39, needed for
  reorderable recovery): v1 opt-in `commutative` annotation on service
  operations, discharged the same way. Without it, revl only promises the
  paper's LIFO guarantees, which is exactly what the runtime delivers anyway.

## 7. Compilation model

```
.rvl source ──parse──▶ AST ──check──▶ typed AST ──link──▶ composition
                                        │                    │
                                        ▼                    ▼
                              per-component lowering   manifest (G2/G3)
                                        │
                                        ▼
                        backend: cordis-py component (v0)
                                 wasm component (v1)
```

Lowering (v0, cordis-py backend):

- `component` → a plugin dict `{"name", "inject", "apply", "Config"}`;
  `requires` → `inject`, `config {}` → a schema, body → `apply` compiled to an
  async generator whose `yield`s are the inverses, landing exactly on
  `ctx.effect`'s iterator protocol, so divert-at-boundary comes from the
  runtime for free.
- `provide` → `ctx.provide`/`ctx.set` with the derived withdrawal inverse.
- Service method calls on required capabilities → calls through the committed
  view (`ctx.<name>`), which is what keeps them readable during teardown.
- `emit` → plain call (tracked as `id`), `compensate` → accumulator push typed
  apart in the manifest.

The backend contract is small (install effect with inverse; provide/read keys;
reactive refresh) and documented, so backends are swappable: this is what
makes the Wasm tier a codegen project rather than a redesign.

## 8. Backend tiers ("shouldn't it compile to native?")

Deliberately not, and not first. The paradigm's hardest runtime requirement is
*unloading code and reclaiming everything it owned*. Raw native (`dlopen`/
`dlclose`) offers no per-component heap, no reclamation guarantee, and no
confinement; it is the paradigm's known-hard case, and rebuilding a hardened
lifecycle runtime is precisely the multi-year cost this project's architecture
avoids (§2.5).

| Tier | Backend | What it proves |
|---|---|---|
| v0 | cordis-py | the semantics and the checker, on a runtime we have hardened ourselves and whose paper-conformance suite doubles as ours |
| v1 | Wasm component model | performance *and* enforcement: imports-at-instantiation are coeffects made physical, instances drop cleanly, and confinement stops being advisory |
| n/a | raw native | non-goal until something the Wasm tier cannot do demands it |

Precedent: Rust bootstrapped on OCaml, Kotlin on the JVM, TypeScript on JS.
Hosted first is how languages are born; native is graduation, and for this
paradigm the graduation target is Wasm, which is "native" with the two
properties we cannot give up (confinement, reclaimable instances).

## 9. v0 milestone

**One checked component compiles, links, runs, hot-swaps, and provably
reverts** on cordis-py, and each guarantee G1–G8 has a test that shows a
program *rejected* (or an outcome forced) that the library version accepts:

1. Grammar + parser (hand-written recursive descent; the grammar is small).
2. Checker: rows, modes, effect/emit classification (G1, G4–G6, G8).
3. Linker: composition manifest (G2, G3).
4. Codegen: cordis-py backend (§7).
5. Demo: `PgDatabase` (stubbed pool) + `UserCache`: swap the database
   provider at runtime; observe the cache deactivate → reactivate; unload
   everything; assert the environment is exactly recovered.
6. Negative suite: one minimal source file per guarantee, each failing to
   compile with a good error message. **The error messages are a deliverable**:
   a research language earns readers through its rejections.

Out of scope for v0: realms/interception, `verified`/`commutative`
annotations, Wasm tier, self-hosting, editor tooling beyond syntax
highlighting.

## 10. Open questions

- Surface syntax for *replacing* a provision (rolling update / service broker,
  paper §6.2): language construct or library pattern on top?
- Should `config` changes be diffable in the language (reload-on-change per
  field, like the Cordis loader) or always restart-the-component in v0?
- How much of the linker's manifest should be a stable, documented format?
  (It is the natural interchange point with agent harnesses that want to admit
  components at runtime.)