# revl - the vision, and the honest scope of the claim

This is the "why" companion to [DESIGN.md](../DESIGN.md) (the what) and
[docs/syntax-2.0.md](syntax-2.0.md) (the how). README links here for the
*honest scope* of the "future of programming" framing; this file is that
honesty, kept deliberately small.

## What revl is for

revl exists to make **dynamic composition safe by construction**: loading,
unloading, and hot-swapping components in a running system, where "unloading
leaves no residue" and "dependencies stay coherent" are compile-time
guarantees (G1–G8) rather than runtime discipline. It is the language-level
realization of the [Cordis paradigm](https://github.com/cordiverse/paper):
the paper proves strong metatheorems, but every one rests on hypotheses no
library can enforce (confinement, witnessed inverses, declared-only access,
acyclic provisioning). revl's job is to move those hypotheses from *runtime
discipline* into the *type system* - the jump C++ RAII made to become Rust's
ownership. See DESIGN.md §1 for the hypothesis-by-hypothesis table.

The second motivation is forward-looking and is where the "future of
programming" phrase comes from: if components are increasingly written by AI
agents, then *machine-checkable safety of a generated component before it
self-deploys* matters more than syntax familiarity. revl is designed to be a
language such a harness could require its own components to pass - the
generate → check → run loop closes inside one file (`test`/`verified`,
syntax-2.0 §7), and the checker's totality lets a corpus be
compile-verified rather than hoped-for.

## One language, six tiers

The same checked front-end lowers to a family of hardened runtimes rather
than to raw native code (DESIGN.md §8 explains why native is deliberately not
first - the paradigm's hardest requirement is reclaiming everything a
component owned, which `dlopen`/`dlclose` cannot promise):

The `conformance today` column is **generated**, not written: it is the
per-tier totals of the conformance register, which also generate the matrix in
[conformance.md](conformance.md). `ok` is a construct the emitter produces,
`limit` a deliberate tier limit, `gap` a construct the emitter has no case for.
A guarantee that moves between those three moves this table too. Regenerate it
with `make docs-gen`; never edit the block by hand.

<!-- docgen:vision-tiers begin -->
| runtime | tier | conformance today | what it proves |
|---|---|---|---|
| cordis-py | reference | 61 ok / 0 limit / 0 gap | the semantics + the checker, on a runtime whose paper-conformance suite doubles as ours |
| cordis (TypeScript, v4) | portability | 61 ok / 0 limit / 0 gap | the same IR runs unchanged on a second host |
| cordis-rs (Rust) | spike | 61 ok / 0 limit / 0 gap | the backend contract is small enough to target any Cordis runtime |
| cordis4j (Java) | spike | 60 ok / 1 limit / 0 gap | the same contract, on a second spike nobody optimised for |
| cordis-wasm | performance + enforcement | 51 ok / 10 limit / 0 gap | confinement becomes physical (sandbox), instances drop cleanly |
| cordis-go (Go) | third-party runtime | 60 ok / 1 limit / 0 gap | the same contract holds for a Cordis runtime nobody on the project wrote ([stc-go](https://github.com/0xdenny218/stc-go)) |
<!-- docgen:vision-tiers end -->

One `.rvl` source, one IR, six emitters. The [2.0 roadmap](v2.0-roadmap.md)
tracks per-tier coverage.

Where each "what it proves" is actually proved - a claim in this project gets
a command or it gets softened:

| tier | gate | note |
|---|---|---|
| cordis-py | `cd backends/python && .venv/bin/pytest -q` | R1–R5 against the real runtime; needs `setup.sh` |
| cordis (TS) | `cd backends/typescript && npm ci && npx vitest run` | same IR, second host |
| cordis-wasm | `pytest backends/wasm/test_v3_emit.py tests/test_wasm_backend.py -q` | executes on real `wasmtime`; skips without it |
| cordis-rs, cordis4j | `pytest backends/rust/test_emit_rust.py backends/java/test_emit_java.py -q` | needs cargo + a JDK; skips loudly otherwise |
| cordis-go | `pytest backends/go/test_emit_go.py -q` | emitted code executes on real stc-go under `go test`; skips loudly otherwise |
| the formal backbone | `make formal` (`sh formal/scripts/run_gate.sh`) | Lean 4: `formal/`, a layering gate plus an axioms gate (no `sorry`, no project-defined axiom). G2, G3 and G7 are `full`; G4, G5, G6, G8 and G9 are also `full`, at the granularity `formal/STATUS.md` states per row (the G4 and G8 shape-level statements are marked weak, and G6 is head-granularity); G1 is `partial`. `formal/STATUS.md` is the per-theorem ledger, and it names each gap. Runs as CI's `formal` job |

Those commands are themselves resolved against the tree, by
`python3 tools/check_vision_claims.py` in CI's required `lint` job: the
directory a `cd` names, the files a `pytest` line lists, the `make` target, the
script a `sh` line runs and the package an `npx` tool comes from all have to
still be here, so a rename or a move reds rather than rotting. The same tool
resolves this file's links and backticked paths, and re-checks the generated
tier table above. It does not RUN the commands, deliberately: the suites they
name are required CI jobs already, and a `lint` job that provisioned cargo, a
JDK, Go, node, wasmtime and elan to re-buy that answer would be narrowed the
first time it got slow. CI runs them; this keeps them pointing at something.

What every tier can and cannot *express* is measured by
`python3 tools/conformance.py` and recorded in
[conformance.md](conformance.md); `--validate` additionally hands each tier's
output to that tier's real compiler. Composing tiers across a process seam
(`--placement`, [interop-bridge.md](interop-bridge.md)) is demonstrated by the
`demo/bridge_*` scripts and not covered by a test - only the static
transport-safety verdict is (`tests/test_distribute.py`).

## The honest scope - what this does *not* claim

`revl_act` accepts only declared arguments, and its effect gate acts on the
checked operation rather than the model's reasoning. Whether reasoning is
visible to the host, hidden in unreadable tokens, or unreadable at all does not
change that decision. This does not block information in an allowed argument
or establish that an explanation is true. `tests/test_tool_loop_act_1708.py`
shows that an undeclared `reasoning` argument is refused by name while the
bare call keeps its effect class and outcome.

Admission applies before a candidate is activated, but revl does not re-admit
prompt, memory, or skill text whenever a harness rewrites it in place. A
checked revertible effect must have a well-shaped inverse; the checker does
not prove that every inverse is semantically correct. `tests/test_admit_approval_gate.py`
exercises the admission boundary, and `tests/test_verified_effect.py` tests
selected inverse round trips and names their limit. Prompt text and memory
content remain outside revl's checks; versioning and reviewing those artifacts
belong to the harness built on revl.

- **Not a general-purpose application language.** revl writes *components*;
  a host application assembles compiled components. Stratum 1 is a
  TypeScript *subset*, chosen to make a model's strongest priors correct,
  not to be a full TS.
- **Semantic inverse correctness is not decided in general.** The checker
  proves an inverse is *present and well-shaped* (G4), and derives teardown
  correctly for compositions of checked primitives; proving an arbitrary
  `undo` truly reverts its effect is undecidable and stays opt-in
  (`verified`, DESIGN.md §6).
- **The extern boundary is trusted, not verified** - but it is *enumerable*
  (G8, `revl audit`): revl cannot check foreign code, only force every escape
  hatch to be declared and auditable. A host's other tools need their own
  classification; see [the substrate-boundary rule](substrate-boundary.md).
- **The calculus's metatheorems transfer by construction, they are not
  re-proved here.** The research claim is a *surface language whose every
  well-typed program satisfies the calculus's hypotheses* (DESIGN.md §5), not
  new type theory. What IS proved here, in Lean, is part of revl's own
  admission judgment: G2, G3 and G7 are `full` in `formal/`, and so are G4,
  G5, G6, G8 and G9 at the granularity their ledger rows state (the G4 and G8
  shape-level statements are marked weak, and G6 is head-granularity). Every
  full row is axiom-gated, with non-vacuity witnesses and, where the ledger
  records one, a differential oracle against `src/revl`; G1 is `partial`, for a
  named modelling reason. `formal/STATUS.md` is the ledger, and it is written
  to be read gap-first.

The pitch, kept honest: **Cordis has revertible effects as a discipline; revl
makes them a type system.** Everything beyond that is roadmap, not claim.