Limits and measurements

Carried from docs/limits.md on 30 Sept 2026; the file is the source.

Limits, as of 27 September 2026

What the language, the verifier, the generated services and the writer stage do not do, with the numbers behind each statement. Dated because items below are being worked on.

Verification is not proof

verify runs examples, scenarios and bounded random testing: sampled unit states, random walks of contracts, random walks of flows, sampled commutativity pairs. It finds states that break rules; it does not prove none exists. Four classes of bugs are outside it by construction (wrong or missing rules, a body that does nothing, a carried value with no stated property, trusted code and the runtime); two of them now have a check, outcome reachability and contract-level ensures. See docs/blind-spots.md. Measured on the number pool: authored checks in the language killed 9 of 12 planted bugs against 11 of 12 for hand-written Rust tests; the three survivors were rules nobody had written down. Depth matters: a program that passed at 1,000 iterations failed at 3,000 (a world-derived column drawn freely inside a unit check). Run deep_regression.sh before a release.

What is trusted

Anything inside impl { … }: functions with Rust bodies and effects. The verifier checks what the program does with their results, not the Rust.

Scale of evidence

Verification is partitioned (reference §19): after a flow, only the invariants and derived columns over units the flow can change are re-checked, and a flow’s walk draws from its component’s flows. On the shop and the tracker that is worth little, because every flow of both goes through one unit (Activity), so both are one component, and the invariant checks were never the cost: the shop at 3,000 iterations went from 19.4 s to 17.0 s in the interpreter and from 47 s to 45 s through the compiled verifier with -O; the tracker from 7.7 s to 7.0 s and 32 s to 32 s. The value model (ROADMAP item 2) then took the compiled shop from 45 s to 16 s and the tracker from 32 s to 17 s on the same day, each pair measured back to back: rows read in place, strings compared without copies, ids sampled without collecting, the walk snapshotting only the units a flow can change, single-call flows not staged and the before-state kept only for ensures. Later the same day a contract case stopped copying its unit, measured in a declared quiet window (the other seats idle, load recorded per round, medians of five interleaved rounds): compiled shop 15.5 s to 13.9 s and tracker 13.4 s to 10.6 s, reproduced by the director in its own window within a tenth of a second; the interpreter single-threaded at 1,000 iterations 26.8 s to 27.1 s on the shop and 11.8 s to 12.1 s on the tracker, within 2%, because its copies come from its callers’ snapshots (ROADMAP.md, item 2). With one job per core the interpreter’s times swing by half between rounds under load from outside the seats, so no multi-job size is recorded. A single unit’s local check takes 0.3 to 3 s. Nothing has been written in the language at ten thousand lines.

Performance of emitted code

A multi-call atomic flow stages the units it touches; a contract case copies nothing of its unit unless one case writes the same field twice (then that field) or its ensures uses unchanged() (then the unit); tables are vectors with linear lookup. A service loads only the units a flow or view touches, so the cost is the size of those units, not of the tenant. The number pool runs about 330,000 flows per second in a release build on a world of eight rows. Cost grows with world size, not with the change: tenant-scoped worlds of thousands of rows are fine, millions are not. What remains is in ROADMAP.md, item 2; none of it touches the language.

Generated Rust

Compiler output: a mechanical translation plus the verification harness. Product-only output is about twice the size of the source and roughly four times a hand-written crate, because of the clones and the generic table helpers. Correct, compiling, non-idiomatic.

Density

Measured on the number pool: contracts are 0.53 of the hand-written crate’s logic by Halstead volume; with scenarios and fixtures the whole artefact is 0.3 to 0.4 of it, near the floor, because guards and ranking keys are the decisions themselves. Algorithms in the computation layer are at parity with Rust (the prelude’s heap: 386 tokens against 371).

The language

• No floats, no bytes; money and time are ints with a scale.
• In the core, no while, no recursion, no mutation outside deltas and function blocks, no effects except through effect declarations; recursion, while, unbounded strings and lists and self-containing rows exist only behind sealed fn and sealed row (reference §7), pure, checked by examples, run under a step budget, never sampled. By design: every function is total.
• Rows do not hold maps. Lists inside rows have no stored form.
• Strings compare by bytes; substr and find count characters.
• Effects return scalars, strings, options and lists, not rows or maps.
• No user interface layer; routes expose JSON.

Parts

A part is a second declaration of a unit holding only contract bodies. It cannot add state, fixtures, invariants, derived fields or machines; its examples may name the interface’s fixtures. A part is checked with its interface, never alone. Inside a unit’s local check a world-derived column is drawn freely within its type, so a bound on the column belongs in the row (open_issues: int(0, 99)), not in a unit invariant.

The writer stage

vishy write writes one request per unit against a stub interface, checks each part locally, retries the contracts the check names with two candidates, assembles, verifies, and repairs the contracts the whole-program verdict names. Measured on the tracker, eight units and 56 contracts, DeepSeek V4.1 Flash and V4 Pro on Baseten: 18.4 s from interface to a verified program (all parts written in 9.3 s, one repair round). A change round on the same program (five cross-cutting changes, one new unit, nine new contracts, three row changes): 2 min 9 s of interface authoring, then 12.3 s to a verified program with the existing parts kept or repaired in place, twelve contracts rewritten and nothing else. The thirty-unit shop, 96 contracts: 26.4 s from a cold directory to a verified program (parts 19.8 s, six contracts retried once, no repair); the earlier Python stage on the same design: 23.4 s with the interface amended by hand during the run. Limits: units of six or more contracts are written in two halves, and nothing larger is split further; a reply cut by the token limit costs one more request; scenario failures name a flow, not a contract, so they are reported and not repaired; a failing contract after the retry rounds is reported and the program is not assembled; a checker failure names every refused contract by checking each alone, at one parse and check per contract. The interface author is a person or a strong model; the stage does not design.

Storage and the door

SQLite and Turso: whole-table rewrite on save. Events are handed to effects::handle in-process and, when the program declares deliver, written to a persisted outbox and delivered at least once. Migrations carry a store across a row change one version at a time (a tenant several versions behind runs each version’s migrate in order); a rewrite rebuilds the whole table; only the tables Vishy created, only per-row expressions, no batched or zero-downtime procedures. Deliveries are at least once: webhooks, mail through an HTTP mail endpoint (VISHY_MAIL_HOOK, not SMTP), or a declared effect wrapping any crate; a delivery that fails 20 times stays in the outbox for an operator; there is no ordering guarantee across events. Typed clients and views exist. A view is sampled for panics, not for the right value: only its scenario steps say what it must return. A flow or a view loads whole units, not the rows it needs: a view over Issues loads every issue of the tenant and filters in memory; pushing the filter into the store’s query is the next step. Route arguments are scalars, options, enums and lists of those; a row cannot be passed as an argument.

Namespaces and packages

No registry; dependencies are paths or git tags. One version per package name, conflicts refused, no lockfile. Names may not contain __.

The toolchain

Two verifier paths with the same verdict: the compiled verifier (emit, rustc, run) and the interpreter (vishy verify), which walks the syntax tree with the same sampler and random sequence; tests/verify_differential.sh holds them to the same first failure. The interpreter is the faster path for per-part checks; for whole programs at 3,000 iterations with one job per core it was faster on the tracker and slower on the shop in the one clean round measured (tracker 8.0 s against 10.6 s compiled, shop 17.9 s against 13.9 s), a size not yet held to the quiet-window rule. The playground’s checker and the writer stage use the interpreter only.

The numbers, measured when the book is checked

The four numbers below are not typed into this page. A script under book/numbers/ prints each one from the repository, and tests/check_book.sh runs the scripts again and fails when this page shows a number the repository no longer has.

The compiler and its command line are 8331 lines of Rust, the files in compiler/src and cli/src, and they are the code that the next number’s checks are written against.

The compiler’s hand-written checks, the scripts under tests/ and the small programs beside them, are 3331 lines, to be read against the compiler’s lines above: that is how much of the compiler’s specification lives in a suite, one chosen point at a time.

The tracker’s interface, apps/tracker/interface.vish, is 1123 lines, compared with the 1,123 that the scale-of-evidence table above gives for it on 27 September 2026; a difference would mean the tracker changed after that table was written.

Of those lines, 357 are inside examples blocks and scenario blocks, compared with the whole interface above: they state behaviour by example, the part a test suite would hold, and the rest of the interface (the rows, the contract headers with their outcomes, the flows) is the part a suite has no place for.