Learn
Plain explanations of the parts Onus is built from, for a reader who has never met them. Each is one screen — what it is, why Onus uses it, one small example, a link to the specification — and none assumes another has been read.
Plain explanations of the parts Onus is built from, for a reader who has never met them. Each is one screen — what it is, why Onus uses it, one small example, a link to the specification — and none assumes another has been read.
What must be true before a function runs, what it promises when it finishes, and what stays true through a loop — checked, not commented.
spec §5Every contract becomes a small logical statement the compiler must establish. A solver decides each one; what it cannot decide becomes a runtime check.
spec §12A type narrowed by a condition. An integer that carries proof of its range wherever it goes.
spec §3.2What a function does beyond computing a result, listed in its signature. A callee's effects must fit inside its caller's. No `may` clause means pure.
spec §6An unforgeable value that grants access to a resource. It can be handed down and narrowed, never acquired or widened.
spec §8A named property that travels through the call graph. Where nobody can check it, `assume` records that trust entered, and why.
spec §7Name an entry point, state what everything reachable from it may do, must guarantee and may assume, and have the whole region checked at once.
spec §9Every obligation's state, every assumption, every runtime-check site, every capability's origin. What the reviewer reads instead of the code.
spec §11, §12.2Readable anywhere, constructible only in its own module. A value of the type is evidence that the module's check ran.
spec §3.10Exactly one way to format any program, enforced by the compiler. Diffs become semantic; a model never spends effort on layout.
spec §2.2Ordinary Onus that the compiler runs while checking. How a library validates your SQL at compile time without a macro or a plugin.
spec §3.8Every module is draft, hardened or critical. Nothing at a higher zone rests on a claim from a lower one. Promotion is earned, not declared.
spec §21 (change log 3)Drives a model against the compiler until every obligation is proved or checked. Edits bodies; never edits a claim.
loop specThe review tool. Renders the ledger, path reports and interface diffs; the place a person approves, answers counterexamples, and decides what the model does next.
spec §15