The reference

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

Reference

One section per feature. Each example is small enough to paste into the playground; the longer ones are in docs/examples/ and tests/*_ok.vish. The compiler knows a small core; the rest is a prelude written in the language.

1. A program

A program is declarations at the top level: rows, enums, events, functions, units, flows, invariants, derived fields, scenarios, routes, effects, and rust dependencies. It may span files and namespaces. The one thing every program has is at least one unit; the smallest useful one is a unit and a scenario.

2. Types

Literals of money, instant and duration are plain ints. [] and map() are empty literals typed by their context.

3. Rows

row Task { id: id, title: string(64), status: Status, created: instant, closed: option<instant>, tags: id[4], home: option<Address> }

A field may be a scalar, a string, an enum, an option of one, a list of scalars, another row, or an optional row. Rows nest but never recurse. A row kept in a keyed table needs an id: id field. Row literals name every non-derived field: Task { id: 1, title: "a", … }; a field whose value is a variable of the same name may be written once, Shipment { id: shipment, order }.

4. Units and state

unit Todo {
    caps storage, outbox;
    state tasks: Task[8];
    state next: int = 1;
    state prices: map<id, money(2)>;
    fn open(t: Task) -> bool = t.status == Status.open;
    invariant all(t in tasks: as_int(t.id) < next);
    contract …
}

A unit owns its state and nothing else may touch it: only the unit’s contracts change it, which is the language’s visibility rule. state fields are tables, lists or scalars with optional initial values; tables start empty. A unit may hold functions that read its state, one invariant (combine with &&) that must hold after every contract call, fixtures, machines, derived fields and a commutes declaration. caps names capabilities: outbox allows emit, storage makes the state persist.

5. Contracts

contract withdraw(amount: money(2)) {
    case amount <= 0 => fail BadAmount;
    case amount > balance => fail Insufficient;
    else => Ok: balance -= amount;
    examples { { balance: 500 } (200) => Ok { balance: 300 }; { balance: 100 } (200) => Insufficient; }
}
contract bump() => Ok: n += 1;                     // one guardless case: no block
contract level(item: id) -> int { outcomes Level(n), fail Unknown; }   // a stub: outcomes declared, no cases
contract read() -> int => Value(n);

Cases are tried in order; the first guard that holds decides; else is the catch-all. A case names an outcome, or fail Outcome, which changes nothing and aborts an atomic flow, or stop Outcome, a success that ends the flow at this call (its writes and the earlier steps’ commit; the later steps do not run; no value). A stub declares them the same way: outcomes Added, stop AlreadyDone, fail Exists;. An outcome’s kind is one for the whole program: a name is a success, a failure or a stop everywhere it appears, as fail has always been. A contract of a unit that declares caps ids may say uses ids; and call fresh() in its cases: each call is a new id above every id the caller knows (the whole world inside a flow, which must say uses ids; the unit alone in an example or a sampled check, where the ids are 1 + the largest present, in order), so a contract can create one row per element of a list (fold(w in winners, acc = []: append(acc, Sale { id: fresh(), … }))) and answer their ids, and the door passes no ids for rows it does not choose. A carried value is written inline, Found(expr), with the return type after -> (default int); the value is computed on the pre-state. Outcome names are yours; the same name means the same thing everywhere.

Deltas after : say what changes and nothing else changes. Right-hand sides read the pre-state.

A keyed table is never assigned whole (t := [...] is refused): rows enter with +=, leave with -= or remove, and change with t[k] := row, t[k].f := e, t.f := e or t := for x where p => row.

Implicit outcomes, never guarded by hand: Unknown for a missing key, Exists for an inserted key that is present, Full for a table past its bound, WrongStatus for a move a machine forbids. They may appear in examples and scenarios.

Case bindings compute a selection once: case any(n in numbers: ok(n)) => let n = best(x in numbers: ok(x) by (x.added)); Picked(n.id): numbers[n.id].used := true;.

Examples are {before} (args) => Outcome[(value)] [{after}]. A state literal lists the fields that differ from the initial values, so {} is the initial state; a fixture name may stand for a state (Two (1, 5) => Ok Two with { … }). An example with no after-state means nothing changed, and the verifier enforces it. Failures never have after-states.

ensures adds a check on the post-state: items := heap_pop(items) ensures perm(append(items, result), old(items)); with old(f), result, unchanged(), emitted([…]).

Contract-level ensures. ensures expr; as a line of the contract (a stub’s or a body’s) is checked after every successful case, with result the carried value (the property then applies to the cases that carry one), bare fields the post-state, old(f) the pre-state, unchanged() the whole unit. Several lines conjoin. An interface’s contract-level ensures survive the merge with a part, so the part’s cases are held to them whatever the writer wrote; a part may add its own. See docs/blind-spots.md.

Deltas apply in order on the old state’s values; a column delta (t.f := e, t.f += e) skips a row that an earlier delta of the same case removed.

Stubs. A contract with outcomes A, fail B, C(value); and no cases is an interface stub: it declares the outcome shapes so examples, scenarios and flows type-check, and a call reports “not implemented (interface stub)” until a part supplies the cases. A contract has either cases or outcomes, never both. vishy check --interface accepts a program only if every contract is a stub.

Parts. A unit may be declared twice across the inputs: the interface, with state, fixtures, invariant and stub contracts, and a part, unit Name { contract … { cases; examples { … } } }, holding only contract bodies. The compiler merges them: the part’s header must equal the stub’s (names, bounds, return type, uses); the merged contract has the part’s cases, the stub’s declared outcomes and the examples of both, and the checker requires the cases to produce every declared outcome with its fail and value shape and nothing undeclared (the implicit outcomes excepted). A part’s examples may name the interface’s fixtures. A part with state, a body for a contract the interface does not declare, or a second body for the same contract is refused. See docs/toolchain.md, “Parts and the writer stage”.

6. Expressions

Arithmetic + - * / %, comparisons, && || !, if c then a else b, let x = e in e, match (on an option: some x => a, none => b; on an enum: one arm per variant, or an else), row fields r.f, with(r, f, e), table access t[k] (guard with k in t), len, lookup(t, k), append, range(n), columns t.f with elementwise lifting (jobs.priority > 3 is a bool column), reductions count, all, any, sum, largest, smallest, min, max, abs, clamp, percent, round_to.

Quantifiers bind a variable: all(x in t: p), any, count, first, where(x in t: p) (the matching elements; where(…).id for their ids), best(x in t: p by (k1, k2)) (the match with the smallest key tuple; bools sort false first; ties by id), fold(x in t, acc = e0: body), repeat(n, s = x0: body). There are no list comprehensions and no loops in expressions.

Strings: concat, starts_with, ends_with, contains, substr(s, start, count) (in bytes, like len; a count that ends inside a character includes that character), byte_at(s, i) (the byte at position i as an int, -1 past the end; the one string read that allocates nothing), to_upper, to_lower, trim, find, split, join, replace, int_to_string, string_to_int. Maps: map(k => v, …), get (an option), get_or, put, remove_key, has_key, keys, values, len. Time: seconds, minutes, hours, days, bucket(t, d), as_duration, as_instant.

7. Functions and the computation layer

fn fee(amount: money(2), tier: Tier) -> money(2) = if tier == Tier.gold then percent(amount, 1) else percent(amount, 3);
examples fee { (10000, Tier.basic) => 300; (10000, Tier.gold) => 100; }

fn heap_push(xs: any[], v: any) -> any[] {
    var h = append(xs, v);
    var i = len(xs);
    repeat len(xs) + 1 {
        let p = (i - 1) / 2;
        if i > 0 && h[p] < h[i] { h := swap_at(h, p, i); i := p; } else { break; }
    }
    h
}

A function is an expression, or a block of statements followed by its result: let and var locals (var toks: Token[64] ordered = []; names the type when the value alone does not, as an empty list or none), x := e on a var, statement if with else if chains, repeat n { … } with break. x := append(x, e) and x := concat(x, e) grow x in place in the compiled code; a loop that builds a list or a string is linear. Every loop is bounded, there is no while and no recursion, so every function is total. Top-level functions may carry examples, run by verify. Blocks are for functions only; contracts stay declarative. fn f(…) -> t impl { rust } is the escape hatch: trusted, not verified; its list, row, string, option and map parameters arrive by reference (&Vec<T>, &String), scalars by value. The prelude (stdlib/prelude.vish) provides perm, submultiset, sorted, is_heap, index_of, take, drop, set_at, swap_at, remove_first, insert_sorted, heap_push, heap_pop and the time helpers, all written in the language.

Sealed functions: the general-computation layer

sealed row Node { v: int, kids: Node[] }
sealed fn total(n: Node) -> int = n.v + fold(k in n.kids, acc = 0: acc + total(k));
sealed fn count_to(n: int(0, 100)) -> int(0, 100) { var i = 0; while i < n { i := i + 1; } i }
sealed fn words(s: string) -> int = len(split(s, " "));
examples total { (Node { v: 1, kids: [Node { v: 2, kids: [] }] }) => 3; }

A core function is total: no recursion (direct or through other functions), loops bounded by repeat, every string and list bounded, no return (a block ends with its result expression). That is what makes contracts and rules checkable and lets the compiler know everything. General computation, a parser, a tree walk, anything that needs recursion, lives behind a declared boundary instead: a sealed fn may call itself and other functions, loop with while, leave early with return e;, take and return string and T[] without a bound, and use sealed rows, which may contain themselves (inside a sealed function or row, Node[] is a list of rows, not a keyed table). Sealed rows exist only inside sealed functions: no unit state, contract, flow, event, view or core row may hold one, and a sealed function called from the core must return a core type.

What the seal promises and what it does not: a sealed function is pure (no unit state, no events, no effects) and its result is trusted only to its declared type, so the boundary checks it (an int(0, 9) result of 10 is a failure naming the function). Totality is not promised: verify runs a sealed function’s examples, and every call to it from a contract or flow during a sampled check, under a step budget of VISHY_FUEL steps (default 10 million, spent per call and per loop iteration, the same on both verifier paths); a function that exhausts it, or recurses deeper than 100,000 calls, fails the example or the check it was reached from. Sealed functions are never sampled on their own: their examples are their test. The service runs them as written, budget included.

8. Flows

flow place(qty: int) uses clock, ids atomic {
    let order = fresh();
    let total = Carts.total(order);
    Orders.place(now, order, qty, total);
    ensures Orders.count == old(Orders.count) + 1;
}

A flow is a sequence of contract calls and effect calls, and a transaction: atomic (the default) restores the whole world if any call fails; serial does not. A step written keep Unit.c(…); in an atomic flow commits what the flow has written so far: a later failure restores the world to right after that step, not to the start (the served door then answers the failure with the kept writes stored), so a refused attempt can be recorded before the refusal. A call that answers a stop outcome ends the flow there as a success; ensures is checked only when the flow runs to its end. Units never call each other; only flows compose them. A carried value can be bound with let and passed on. uses clock binds now; uses ids allows let x = fresh();, an id absent from every table. A flow’s outcome is its last call’s. ensures is checked after the flow commits, with Unit.field and old(Unit.field). A scenario or a route may call a contract directly, Counter.bump(), which is an implicit one-call atomic flow.

uses caller binds caller: id, the verified identity of the request: the served door takes it from the bearer token (401 without one) and never from the body, the command line from VISHY_CALLER, a scenario step from as N (as 7 remove_note(1) => NotOwner;), and the verifier samples it like any argument. A flow that does not use caller cannot name it; a body that passes an identity in is what uses caller replaces.

9. Views

A view is a read over the world, declared in the language so that who sees what is a rule the compiler holds:

view my_issues(project: id) uses caller
    = where(i in Issues.issues: i.project == project && any(m in Members.members: m.user == caller && m.project == project));
view issue_count(project: id) = count(i in Issues.issues: i.project == project);
route GET "/projects/{project}/issues" => my_issues(project);

view name(params) [uses caller] = expr;. The expression is typed like a world invariant, with Unit.field in scope, the parameters, and caller when the view uses it; its type is inferred and may be a list of rows, a row, an option or a scalar (not a unit). A view never writes: there are no deltas, and a route to it must be GET. Scenarios assert on views with name(args) => Value(v), as N before a step setting the caller. The verifier evaluates every view on reachable worlds with sampled arguments and fails on a panic (an empty first, an absent key), counted among the sampled checks; it cannot judge whether the value is right beyond the scenarios and the examples. The door serves a view route from the stored world without a transaction, as {"ok": true, "value": v}, and pages a list with limit and offset query parameters ("total" and "offset" alongside); a view served by a route cannot name a parameter limit or offset. The clients get one method per view route with the value’s type. A view is interface-owned: writers never write one.

10. World invariants and derived state

invariant all(l in Stock.levels: l.reserved <= l.on_hand);
derived Ledger.cash = sum(Payments.payments.captured) - sum(Payments.payments.refunded);
derived Stock.levels.reserved = for l => sum(where(x in CartLines.lines: x.sku == l.sku).qty);

A top-level invariant names units’ state and must hold after every flow; the verifier samples only worlds that satisfy it. A derived field is defined by an equation and maintained by the compiler after every call or flow, never assigned; inside a unit, derived total: int = sum(accts.bal);. A unit’s invariant may not mention a world-derived field of that unit; state such a rule at the top level.

11. Machines

machine orders.status { start Status.placed; Status.placed -> Status.paid; Status.paid -> Status.shipped; Status.placed..Status.paid -> Status.cancelled; }

Declares the legal moves of a row field; a delta that moves it any other way fails with WrongStatus. Staying in place is a move too and needs its edge. One contract advance(k, to) replaces one per transition.

12. Commutativity and fixtures

commutes { started, ended }; makes the verifier apply sampled pairs of those contracts in both orders from a sampled state and report when the orders disagree. fixture Two = { accts: [ … ] }; names a state for examples.

13. Scenarios

scenario checkout {
    at 1000 submit(7, 42, Kind.check) => Queued(s);
    at 1500 started(s) => Started;
    status(s) => Status("running\n");
    Cache.lookup(42) => Hit(s);
}

A sequence of flow or contract calls from the initial world with the outcome each must produce; at N sets the clock; as N sets the caller for a flow that uses caller; a bare name as the expected value binds the carried value for later steps; Outcome(_) accepts any value. Run prints the trace; verify stops a scenario at its first wrong step and shows the world.

14. Namespaces and files

A program may be many files. A file’s namespace is namespace x; at its top, else the directory it was given in, else the root. Inside its namespace a declaration is bare; elsewhere it is money::Fee, imported with use money::Fee;, use money::Fee as F; or use money::*;. Rows, enums, events, functions, units, flows and effects are what a namespace exports; state and contracts belong to their unit, so there is no pub. The prelude is visible everywhere. Names may not contain __. A unit may be split across files as an interface and a part (section 5).

15. Packages

A directory with package.vishy (name, version, optional namespace, dep x = path "…" or dep x = git "…" tag "…") is a package; dependencies resolve recursively, one version per name. vishy interface prints the public surface; vishy diff old new classifies a change as patch, minor or major and refuses a version that does not cover it.

16. Storage and capacity

caps storage; on a unit makes its state persist and changes nothing else. vishy schema prints the SQLite schema; vishy service writes a crate that runs each flow as a transaction over SQLite or Turso. The bound in Row[8] is for verification; a rule about capacity says cap(rows), which is the bound when verifying and unbounded in a service.

17. Migrations

A program with stored units declares version N;. When a row or a stored scalar changes between versions, the compiler carries the store forward, deriving what it can and requiring the rest to be written:

version 2;
row Customer { id: id, full_name: string(64), tier: Tier, greeted: int }
migrate Customer from 1 { full_name = old.name; }
    examples { { id: 1, name: "Ada" } => { id: 1, full_name: "Ada", tier: Tier.basic, greeted: 0 }; }

Derived without a declaration: a field added with a default (an enum’s first variant, 0, the empty string, none), a widened bound, a new table, a new scalar state. Never derived: losing data. A removed field needs drop field; inside the migrate block, or an assignment that reads it (a rename), and the compiler says which when a field of the same type appeared alongside. Written as migrate Row from N { field = expr; … }: a rename, a recomputed field, a narrowed type; old is the row as version N declared it, typed against that declaration, so old.name is an error when version N had no name. migrate drop Unit; allows a vanished unit’s tables to be dropped. Examples give an old row and the new row it must become; they run at check time. The verifier does not sample migrations.

vishy check new.vish --from=old.vish types the migrations and runs the examples; vishy service new.vish out/ --from=old.vish emits a service whose migrate carries a store at version N forward exactly once and records the version (schema_versions); a service built without --from refuses a store at another version and says which program to build it from. Not covered, by design: tables Vishy did not create, migrations that need data from other tables or outside, batched zero-downtime backfills, and anything a per-row expression cannot say; those are written by hand as an effect or a script. A rewrite (a rename) rebuilds the whole table; on a very large table run it in a window.

18. Routes and effects

route POST "/submit" => submit(client, hash, kind);
route GET "/status/{submission}" => status(submission);

rust serde_json = "1";
effect json_len(s: string(200)) -> int
  impl { serde_json::from_str::<serde_json::Value>(&s).map(|v| v.as_array().map_or(0, |a| a.len() as i64)).unwrap_or(-1) }
  fixtures { ("[1,2,3]") => 3; ("x") => -1; }
flow count(s: string(200)) atomic { let k = json_len(s); Counter.set(k); }

A route invokes exactly one flow; path parameters and JSON fields bind its parameters by name; the response is the outcome, 200 or 409; GET routes may only invoke query flows. An effect is a Rust-backed function with effects, callable from flows and never from contracts. In verification it returns a fixture’s value or a sampled one; in a service build it runs the Rust with the declared crate. The language has no I/O of its own: effects are facts a flow emits and a runtime performs.

Deliveries. deliver Event to webhook "https://…";, deliver Event to webhook env "NAME";, deliver Event to mail "ops@example.com";, deliver Event to effect name; say where an emitted event goes. A program declares the destinations; the service does the delivery: one outbox row per (event, delivery) written in the same store transaction as the flow’s state change, so an event is never lost and never recorded without its cause; a drainer posts each row as JSON with an Idempotency-Key (<tenant>-<row id>, stable across retries so the receiver can deduplicate), marks it delivered on a 2xx, and otherwise retries with exponential backoff (1 s, 2 s, 4 s, … up to 5 minutes, at most 20 attempts). Delivery is at least once. A webhook target is a URL or the name of an environment variable holding one; a mail target is an address, delivered by posting {to, subject, event} to the endpoint in VISHY_MAIL_HOOK; an effect target is a declared effect (body: string(n)) -> bool, called by the drainer with the event as JSON, delivered when it returns true, retried when it returns false or panics. The effect is how any crate becomes a destination: a broker client, a queue, a mail library, with the Rust inside the effect’s impl and the choice of destination one line of Vishy:

rust lapin = "2";
effect publish(body: string(4000)) -> bool impl { /* the AMQP client */ } fixtures { ("") => false; }
deliver OrderPlaced to effect publish;

The verifier does not deliver anything; scenarios and ensures emitted([…]) are what check that the right events are emitted.

19. Verification

verify runs every example, every scenario, sampled checks of every contract against its unit’s invariant and ensures from random and reachable states, reachable walks of the flows checking atomicity, flow ensures, world invariants and capacities, and commutativity pairs. It reports each failure with the state and arguments that caused it. After the checks it requires reachability: every outcome a contract’s cases can produce, the implicit four excepted, must have been produced by an example or a sampled call, else the case is unreachable or unverified and verify fails. It is bounded random testing, not proof; see Limits and measurements and, for what it cannot see, docs/blind-spots.md.

Verification is partitioned by what a flow can change. A flow’s closure is the units it calls plus every unit a world-derived column carries a change into. After the flow, the verifier re-checks only the world invariants that mention a unit in that closure and recomputes only the derived columns that write one; the others cannot have changed, so their values stand. A flow’s reachable walk draws only from the flows of its component of the unit graph (vishy graph prints the components and, per flow, what its verification touches). Both verifier paths partition the same way and report the same failure, including the invariant’s number in source order.

20. Reserved names

old, out, result, self, staged, outbox, sealed, while, anything starting with __, Rust keywords, and the emitted runtime’s type names.