Environment
Onus is a language plus an environment. The language is the smaller half.
The bet is that trusting model-written code is not solved by a language alone. It takes nine parts, each of which owns one thing and reduces one burden on the person reviewing. Solid boxes are built; dashed ones are specified but not built; dotted ones are intentions.
| Part | Owns | Reduces | Status, 2026-09-05 |
|---|---|---|---|
| Language and compiler | every claim: types, contracts, effects, capabilities, paths | review to reading interfaces | built; being rewritten in Onus |
| The loop | function bodies | prompting to writing a task | built |
| The ledger | what each obligation rests on | “what am I trusting” to a list | built |
| Review tool | rendering the ledger; decisions | reading diffs to reading claims | built; promotion not yet |
| Zones | strictness per module; promotion | one standard for the whole codebase to one per module | specified, not built |
| Targets | JavaScript, native, WebAssembly from one lowering | “does it behave the same” to a differential test | built; WebAssembly untested |
| Task intake | tickets and production failures becoming tasks | triage | not specified |
| Telemetry | which checked obligations fire, and how often | guessing which contracts to tighten | not specified |
| Registry | published interface documents, versioned | trusting a dependency by reading its code | not specified |
Language and compiler. The specification is the contract between the person and the model: pure by default, every effect in the signature, every obligation in one of three states. The compiler is the only checker; there is no linter and no warning level. It exists in TypeScript, and is being rewritten in Onus stage by stage, each stage differential-tested against the TypeScript compiler over the whole fixture suite until the last stage reaches a fixed point.
The loop. The loop turns a task into a change. It assembles the model’s context from compiler output, never from source; runs generate, check, classify until green; and never edits a claim. If a contract cannot be met, it stops and proposes. It is the only part of the environment that talks to a model.
The ledger. Every obligation, its location, its state, and what discharged it; every assume with its justification and whether it has been verified against reality, and when; every capability’s construction site and the configuration it depends on. The ledger is what the reviewer reads instead of the code. Its shape is the path report and the interface document, and it gains a field whenever a new kind of trust is introduced.
Review tool. A static page over the ledger: path view, interface view, ledger view, diff view, counterexample view. It computes nothing. Decisions made in it — approve, reject, accept a proposal, tighten a contract — are meant to flow back to the loop as tasks; in v0 they do not yet, and promotion (drafting the declaration that enforces a convention the reviewer spotted) is unbuilt.
Zones. Every module is draft, hardened or critical; nothing at a higher zone may depend on a claim from a lower one; promotion is earned by regenerating the module’s bodies from its interfaces and finding nothing missing. Specified in change log 3; the manifest, the dependency rule and the hardened modifier are the next compiler work after the rewrite.
Targets. One lowering, two emitters: JavaScript, and native code through LLVM. Every proved obligation emits nothing; every checked one emits a compare-and-branch. onus test --target all runs the examples on both and reports disagreement as a diagnostic. WebAssembly goes through the same LLVM path and is written but untested for want of a toolchain. See §19.
Task intake. Not yet specified. The intent: a ticket — a described defect or feature — becomes a ticket task, whose first output is a proposal for the interface change; only after a person accepts it does an implement task follow. Production failures arrive the same way, through telemetry.
Telemetry. Not yet specified. The intent: the runtime’s panic carries an obligation id and the values involved; telemetry forwards these as repair tasks whose counterexample is the production values, pinned as an example before any body changes. Checked obligations that are hit often and never fail are reported as candidates for proving.
Registry. Not yet specified. The intent: a dependency is trusted by its published interface document, not its source; the registry holds those documents versioned, and the compiler refuses a compatible-version bump that weakens a contract or widens an effect set.
What we haven’t built
As of 2026-09-05:
- Task intake, telemetry, registry. Intentions only, above.
- Zones. Specified on 5 September 2026; no code.
- Concurrency. The language has no story for it. Nothing in v0 spawns, and
nondetis the only acknowledgement that scheduling exists. - A foreign function interface beyond
assume. Host claims let a program say what it needs from the runtime; anything else that crosses into another language is an assumption, and is reported as one. - Decisions flowing back from the review tool, and promotion drafts.
- Constrained decoding in the loop.
onus nextexists; no model runtime the loop talks to can use it yet, so the hook is declared and unused. - Production feedback. A
repairtask may carry a production counterexample; nothing produces one. - WebAssembly, untested.
- The compiler in Onus. Front end, checker and verifier agree with the TypeScript compiler on every source; the reports, code generation and the CLI remain, and after them the fixed point.