Authoring an interface

The guide for the interface owner, included from docs/authoring.md, which is the source; only its third and fifth lines are carried by hand, so that their links work in the book.

Authoring: from a requirement to a checked interface

For a frontier model acting as the interface owner of one application. You receive a business requirement in whatever form it comes and produce three things: a brief, a numbered list of assumptions, and an interface that vishy check --interface accepts. Writers, human or vishy write, take it from there (Building with a team, steps 3 to 5). You do not write contract bodies and you do not design screens.

The guide is in two steps. Step one turns any input into the brief, five lists. Step two turns the brief into the interface. Between them sits the one review checkpoint, used in one of the two modes below. Every rule from docs/agents.md, “Rules for interface authors”, is placed at the step where it applies, with the run that taught it. Every command quoted here was run on 27 Sept 2026 on the handbook’s example, docs/examples/handbook/, and on small refused cases whose messages are quoted verbatim; vishy means target/debug/vishy in the repository (it is not on PATH).

What you receive

Any mix of these:

• Prose. A page or an email: what the product is, what it must do, what it must never do.
• A PRD with user stories. “As a member, I want to cancel my booking, so that the slot frees up”, with acceptance criteria.
• A conversation transcript. People deciding things, changing their minds, leaving points open.
• An ontology module, optionally: entities with attributes, relations between them, shapes (which attributes are required, their types and ranges).

None of these is the brief. The brief is what you write in step one, and it is the only thing step two reads.

The rule that lets you finish: never block

The input will not answer every question. You decide, and you record. A decision is recorded when the verifier will enforce it, because then a wrong guess becomes a failing check for someone who did not make the guess. Three kinds are recorded, as a numbered assumption with the default you took:

1. A number that becomes a bound or a cap. “A room has seats” gives no maximum; seats: int(1, 200) needs one. The input’s own numbers (“slots 1 to 8”) are not assumptions.
2. A rule with two readings that give different scenarios. “Only the holder can cancel”: is there an administrator who can cancel for others? Write both scenarios, keep one, record which and why.
3. A failure the rules require that nothing names. Rule 1 makes a booking of five people in a four-seat room fail; the input never says what that failure is called. Name it (TooSmall), mark it invented. The name is part of the API (a client switches on it), so it is recorded.

Everything else is decided silently: the split into units, field names, example values, fixture names, table sizes used for verification, and every mistake the checker catches, because the checker’s refusal is the record. A silent decision still gets a comment where the reader needs one (a flow’s order of calls that keeps a rule), but no number.

An assumption is written once, in ASSUMPTIONS.md, and cited in the interface as a comment on the declaration it produced:

// assumption 1: seats is int(1, 200); the requirement gives no maximum.
row Room { id: id, name: string(64), seats: int(1, 200), closed: bool }

The comment goes on its own line, before the declaration’s other comments, in the form // assumption N: …, so that one command lists every assumption the interface carries:

grep -n "assumption" interface.vish

Comments in that form parse in every position that takes one: before a row, before a world invariant, inside a unit before a state or a contract, before a flow (run on a copy of the handbook’s interface with five such comments; check --interface still answers ok).

When the input contradicts itself, the later and the more specific statement wins, and the choice is an assumption of kind 2. When the input asks for something the language cannot say, do not invent a construct: write the nearest thing the language has, record the gap in your report, and keep going.

The two modes

• Alone. You run steps one and two without stopping. The assumption list is the audit trail: a reviewer who reads it afterwards sees every decision the input did not make, in the order you made them, each with the declaration it changed.
• With a human reviewing the brief. You stop after step one, hand over BRIEF.md and ASSUMPTIONS.md, and the assumption list is the review agenda: the reviewer answers by number. Then you run step two. A reviewed assumption stays in the list with the answer added (decided by review: an administrator may cancel; see flow admin_cancel); an unanswered one keeps its default. The interface may be reviewed a second time before writers start; agents.md asks for it (“have the interface adjudicated before writers start”), and the checker’s ok is the entry condition for that review, not a replacement for it.

The files are the same in both modes. The mode changes only whether you wait at the checkpoint marked below.

Step one: the brief

The brief is five lists, in BRIEF.md; the third list, what must always hold, is the rules, and they are numbered because the interface will cite the numbers. Every item cites the input it came from (a paragraph, a story, a line of the transcript, an entity) so the reviewer can check it.

1. What exists. The things the product keeps, each with its attributes and, for every quantity, its range. This list becomes the rows.
2. What may be done to it, and with which outcomes. Every action, its inputs, its success, and every way it can fail. This list becomes the contracts and the flows.
3. What must always hold. Every rule that is true of the whole state at every moment, whichever action ran. This list becomes the bounds, the machines and the invariants.
4. What is read. Every screen, report or query, with what it shows and to whom. This list becomes the views.
5. Who may do what. Every action’s caller and the condition on the caller. This list becomes the uses caller flows and the visibility rules inside views.

The handbook’s six-line brief, docs/examples/handbook/BRIEF.md, in this form:

Two assumptions this brief leaves to the author: the maximum number of seats (kind 1; the interface takes 200) and the names of the failures rule 1 and rule 2 require (kind 3; TooSmall, RoomClosed, Taken, all invented). Everything else the six lines decide.

Reading each kind of input

• Prose. Every noun that the product keeps goes to list 1; every verb to list 2; every “always”, “never”, “at most”, “only” to list 3 or 5; every “shows”, “sees”, “lists” to list 4. A sentence that mentions a number puts the number in list 1 (a range) or list 3 (a cap).
• User stories. The “I want” is an item of list 2; the “as a” is its caller in list 5; the “so that” often names a rule for list 3 or a read for list 4. Each acceptance criterion is one scenario step: a call and the outcome it must produce. Keep the story’s id on the item; the scenario will carry it.
• A transcript. Read it to the end before writing anything. For each point, the last decision stands; a point raised and never settled is an assumption of kind 2; a number someone proposed and nobody rejected is a number the input gave, not an assumption.
• An ontology module. Each entity is an item of list 1 with its attributes. A relation becomes an id field on the row that owns the relation (the booking holds room: id, not the room a list of bookings) and a rule in list 3 that the referenced thing exists (the handbook’s rule 1 is that rule with two conditions added). A shape’s required attributes become non-optional fields; its optional ones become option<T>; its ranges become bounds; a cardinality (“at most 4 labels per issue”) becomes a cap in list 3.

What the brief never contains: how anything is computed, which unit holds what, or the name of a counter, an index or a helper. Those are step two’s and the writer’s.

Review checkpoint (mode two stops here)

Hand over BRIEF.md and ASSUMPTIONS.md. Resume when the answers arrive, or at once in mode one.

Step two: the interface

The interface is one file, interface.vish, written against the checker until it answers ok. The order below is the order that produces the fewest rewrites; each part places the rules from agents.md that apply to it, with the run that taught the rule in brackets.

Declare version 1; at the top before anything else. A program without a version is served at version 0 and runs, but the first change to a stored row or a new stored unit is then refused at reload (“the new program declares no version N;”) until the version exists; declared on day one, that first change is a version bump and a derived migration [the privacy ladder, 30 Sept 2026].

2a. Units that own their data

Split list 1 into units so that every row has one owner and no unit needs to read another’s state to decide anything. The handbook’s example has Rooms and Bookings; the tracker (apps/tracker/interface.vish) has nine units for ten rows.

• A fact that two units need is carried by the flow as a value or a bounded list, into the unit that owns the data: let skus = Wishlists.wished(customer); Stock.count_available(skus, location);. A contract never reads another unit, a flow never computes, and a world-derived column takes no parameter. [Experiment ten: the author and the supervisor both missed this and changed the brief instead.]
• A verdict is not a value. A boolean carried from one unit into another, or a bool parameter that stands for another unit’s answer, hides a cross-unit read. The unit that knows decides and fails; the flow calls it first; the next contract takes no flag. Comparing a warehouse id with an order’s location is the same mistake: carry the warehouse’s location in. [Experiment ten.]
• Never name an internal counter, index or helper in the interface (next_line, a sku index): those are the writer’s to choose. [The authoring gate flagged two units of experiment nine’s accepted interface for this.]

vishy graph interface.vish prints the components and, per flow, the units it touches. One component is normal for a small application; the note it prints when one component spans the whole world is worth reading once.

2b. Rows, with bounds

Write every row from list 1. Give every quantity a bound, and mark the storage units with caps storage.

• Bound every quantity by default. qty: int(1, 999), not int. A bound makes a bad value unwritable in examples, unsampleable by the verifier and unarguable at a call; a plain int leaves the guard to every writer and the discovery to luck. [Experiment nine: the one bug found late was a negative quantity reaching a stock level through an unbounded field.] The checker accepts a plain int (run: an interface with seats: int answers ok), so the bound is yours to remember; each bound the input did not give is an assumption of kind 1.
• A derived amount’s domain lives in the row’s type (refunded: int(0, …)): the sampler draws a world-derived column freely inside a unit check and respects only what the type says, and a unit invariant cannot name a world-derived field. [Found by a 3,000-iteration sample on a program that had passed at 1,000.]
• A table’s size (Room[32]) is a verification bound, chosen silently. A rule about capacity in list 3 says cap(rows) and does not repeat the number; then the number is a product cap and an assumption of kind 1 if the input did not give it.
• A row whose field moves through fixed states (open, in_progress, blocked, done) gets an enum and a machine declaring the legal moves; a move the machine forbids is WrongStatus without a guard.

2c. Stubs, one per action, every failure exampled

Write every unit’s contracts as stubs: the header with bounded parameters, the rule as a one-sentence comment, outcomes …;, and examples { … }. No cases: the checker refuses a body in an interface.

b_body.vish:4:5: error: `Rooms.add` has cases; an interface declares outcomes, not bodies (`outcomes Ok, fail Full;`)

• Every rule an invariant states needs an outcome in some contract’s signature. If rule 3 says amounts are positive, some contract must be able to answer BadAmount. [Experiment nine: three signatures lacked one; every writer invented a name for it until the outcome gate refused them.] Go through list 3 rule by rule and name the contract and outcome that keeps each one; a rule with no outcome is either kept by a bound (then say so in the rule’s comment) or is a gap.

• Every declared failure outcome gets an acceptance example. A writer who omits the guard then fails locally and deterministically, instead of when a deep sample happens to reach it. [Experiment nine.] The checker enforces it:

  a_noexample.vish:5:30: error: `Rooms.add` declares `fail TooBig` without an acceptance example that produces it; write the example (it is the rule for when the failure occurs)
  

• Never leave a rule only in prose. “Amount checks are another unit’s job” in a signature’s comment became an invented guard in two experiments. Say it as an outcome, a bound or an example.

• A formula for a carried value is stated through examples, not prose. Prose formulas read as implementation and the authoring gate flags them. Three examples that pin the formula beat a sentence.

• A carried value gets its property in the stub: ensures result == count(…); or the bounds that must hold. Without it the value is checked only on the exampled states; with it, on every sampled one, whatever the writer wrote (docs/blind-spots.md). A stub with a contract-level ensures passes check --interface (run).

• One outcome name has one shape across the whole program, and the brief must obey it too. [Experiment ten’s brief named a new flow’s success Backordered while an earlier account used it as a failure, and asked one flow to fail Held while Held was another’s success; the brief was amended.] The checker refuses the clash:

  c_twoshapes.vish:9:27: error: outcome `Added` is declared differently elsewhere (fail / carried value / type must agree across the program)
  

• Two examples with the same starting state and arguments must agree. If they expect different outcomes, the contract is deciding on a fact it does not hold. The interface check does not catch this (run: two such examples answer ok); the verifier catches it once a part exists, so catch it yourself first.

• A failure the brief lists may be impossible under a rule (a balanced ledger is never Unbalanced; a held order is never paid, so never fulfilled). Then the flow says // Outcome: unreachable under rule:<name> and no contract declares it, instead of an example from a state that cannot exist.

• The implicit outcomes are never declared and never guarded: an absent key is Unknown, an inserted existing key is Exists, a table past its bound is Full, an illegal machine move is WrongStatus. They may appear in examples (Two (9, 1) => Unknown;) and scenarios, and an example that shows one costs nothing.

• Every example’s arguments lie inside the bounds; the checker refuses one outside:

  g_unreachable.vish:6:85: error: example argument for `seats` is outside its type
  

  A failure example has no after-state; a success example whose contract changes state shows what changed.

Fixtures (fixture Two = { rooms: [ … ] };) make the examples short; name a fixture for each state the examples keep returning to.

2d. Flows, carrying values between units

Write one flow per item of list 2, calling the units in the order that keeps the rules of list 3. Give the flow uses caller when list 5 puts a condition on the caller, and pass caller into the contract that decides.

• A rule that couples several units is kept by the flow that commands them, in the order that keeps it, with a comment saying so. close_room clears the bookings before it closes the room; book asks Rooms.fits before Bookings.book. Every flow that commands one of the coupled units and never calls the others says why the rule cannot break: // rule: unchanged because …. The verifier finds the world where it breaks otherwise. The tracker’s interface carries such lines above most of its flows.
• A flow never computes. It binds a carried value, let p = Issues.project_of(issue);, and passes it on. A condition that needs arithmetic belongs in the contract of the unit that owns the numbers.
• A flow that only reads is not a flow; see 2e.
• If the input arrives in installments and a later one changes a flow’s signature or precedence, or adds a rule, restate every flow and scenario that exercises it in that installment’s section, so that nothing kept from an earlier installment calls a flow that no longer exists in that form. [Experiment ten: twenty-five of thirty-one assembly failures were one account’s new rule that no kept flow called.]

A flow’s parameter types should equal the contract’s. The interface check refuses a different type:

j2_mismatch.vish:9:68: error: argument `seats` of `Rooms.add` expects int(1,200), got string(8)

It accepts a wider bound of the same type (run: int(1, 300) in the flow over int(1, 200) in the contract answers ok), so the bound is yours to keep equal; the verifier would find it later as an argument outside the contract’s type.

2e. Views, for everything that is read

Every item of list 4 is a view, with a GET route, and the rule of who sees what inside the expression:

view my_bookings() uses caller = where(b in Bookings.bookings: b.holder == caller);
route GET "/me/bookings" => my_bookings();

• A read a screen needs is a view, not a flow. A flow that only reads still costs a transaction and a contract; a view costs neither, and the rule of who sees what is checked where it is written. A scenario step as 100 my_bookings() => Value([…]) asserts on it. (The tracker predates views and states its reads as query flows; do not copy that.)

2f. Scenarios, from the stories

Every user story, acceptance criterion and rule-with-two-readings becomes a scenario or a step of one: the call, as N for the caller, at N for the clock, and the outcome. A scenario is the product’s behaviour stated once; the verifier stops at the first wrong step and shows the world. The checker types every step against the flows:

d_badstep.vish:10:26: error: scenario `s` step 1 argument `seats` expects int(1,200), got string

Write at least one step that produces each declared failure through a flow, not only through the contract’s example, so the flow’s order of calls is exercised too. The handbook’s a_day_in_alpha reaches Exists, Taken, TooSmall, Unknown, NotHolder and RoomClosed in fourteen steps.

2g. Later changes

A row change on a deployed program is a version bump and, for a rename or a recomputed field, a migrate Row from N { field = expr; } with an example; the compiler derives added fields with defaults and removed fields and refuses what it cannot derive, naming the declaration to write (reference §17). A change to the interface after writers have started goes through the same check and then the handbook’s step 3 again; parts that still pass are kept.

Step two in parallel: the interface as a directory, authors as roles

Measured on 29 Sept 2026 on one application with two products (the fifteenth and sixteenth compiler reports): one author wrote a 111-contract interface serially in 42 minutes; five authors then wrote the second product’s 66 contracts at once in 18 minutes, with no name clash, and the whole program was verified 49 minutes after they started. What carried the parallel work was not the authors talking to each other; they never did. It was three things each author received before starting, and the checker enforcing the rest. Keep it that way as features grow.

The interface is a directory, and the memory. One program, many files, checked as one (vishy check --interface dir/ or the files listed). Each file has one owner role, never a person:

• shared.vish: the enums and carried rows that cross components. The director owns it. An author who needs a new shared row asks; the director adds it, serially.
• one file per component: its rows, units, stubs, fixtures, machines and examples; beside it <component>.assumptions.md, numbered, with the default taken for every number the input did not give and every open point. That file is the replacement author’s memory: a fresh agent given the component file, its assumptions file and the check command continues where the last one stopped.
• flows.vish, views.vish, scenarios/: the director’s. Flows are the only place two components meet, so the joint check lives here.
• ASSUMPTIONS.md at the top: the run’s decisions, the findings, and the reviewer’s answers.

A new feature is a new component file plus additions to the shared file and the flows. The parts already written stay; the write stage writes only new or changed units; a changed row is a version bump with a migrate block (reference §17). Split a single-file interface into this shape before the next feature, not after.

The shared step, written before any author starts. One page:

1. the components, each with its scope in the input (sections, actions, rules, stories) and the contracts the director expects to call;
2. the carried rows and shared enums, in shared.vish, already checking against the existing interface;
3. the taken outcome names with their shapes, generated (vishy interface prints the public surface), never maintained by hand; a taken name may be reused only with the same shape and meaning; a new success that carries a value gets a name prefixed by the component’s word;
4. an id block per component for examples, disjoint from the existing fixtures;
5. the flow’s limits, stated as signature rules, because every author assumes the opposite: a flow cannot loop, so a contract fed by the flow for many things takes a bounded list; a flow cannot build a row, so a contract fed by the door takes scalars; a flow can pass one field of a row it carries (let f = Campaigns.facts(c); Offers.terms_of(f.offer), one level, no arithmetic), so a contract that needs one field of another unit’s answer takes that field, not the whole row [the run’s F6 said the opposite; wrong since 30 Sept 2026, tests/flow_field_ok.vish]; a flow still cannot branch, but a contract can end it early as a success with a stop outcome (a repeated confirmation answers AlreadyRecorded and the payout step does not run), and a step marked keep records before a later refusal (an attempt is noted, then the sale refuses) [item 11 c, 30 Sept 2026]; a flow still cannot loop, but a contract of a unit with caps ids that says uses ids; can mint one id per element of a list with fresh() in a fold, so a flow that creates several rows no longer takes their ids from the door [item 11 d];
6. the boundaries (what is outside, and that its events arrive as flows the door calls), and the check command with a time box.

Without item 5 the run needed a second round: five sets of signature changes sent to the authors after the flows were written. With it, that round does not exist.

The joint round. The director writes the flows, views, routes and scenarios against the components, runs the joint check, and sends every change a component needs to its author as a message, never editing the author’s file (the file’s history must say who wrote what, and a director who edits mid-flight hides whether the author could have done it). Scenarios are written now, before the write stage: in the run, a scenario found a rule three flows had missed that no unit check could see.

What to avoid. Author-to-author collaboration: two agents editing one file, or negotiating a row between them, is what the shared step exists to prevent; the one time it is needed it is the director’s job. A single monolithic interface file once there are two products. Hand-maintained lists of taken names.

The director role. The shared step, the flows, the scenarios, the joint check, the calls on assumptions, and the messages to authors. It is serial, and it is where judgement sits. It is also replaceable: its state is the files and the log, nothing else.

Two more rules from the compiler in Vishy (30 Sept 2026), where two authors wrote the parser’s remaining declarations in twelve minutes: give each author its own scratch directory, because two authors sharing one overwrote each other’s build mid-run and lost minutes to a phantom discrepancy; and when the authors’ oracle is a check script, run it once yourself before the launch, because both authors lost their first minutes to the same harness bug (a script handing three files to a one-file tool).

Running the checker

From the repository root:

vishy check --interface docs/examples/handbook/interface.vish

ok: 2 row(s), 0 event(s), 0 fn(s), 2 unit(s), 6 contract(s), 4 flow(s)

On a refusal the message names the file, line, column and declaration; fix that declaration and run again. Then:

vishy graph docs/examples/handbook/interface.vish

2 unit(s), 4 flow(s), 1 world invariant(s), 0 world-derived field(s): 1 component(s)
component 1: units Rooms, Bookings | flows add_room, close_room, book, cancel | 1 invariant(s)
flow add_room: touches Rooms | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 4 flow(s)
flow close_room: touches Rooms, Bookings | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 4 flow(s)
flow book: touches Rooms, Bookings | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 4 flow(s)
flow cancel: touches Bookings | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 4 flow(s)
note: one component spans the whole world; every flow's walk draws from every flow. Look for a unit that every flow touches.

What the checker catches at interface time, each run on a small case on 27 Sept 2026: a contract with a body; a declared failure without an example; one outcome name with two shapes; a scenario step that does not type; an example argument outside its bound; a flow passing a value of the wrong type to a contract. What it does not catch, also run: a plain int where a bound belongs; two examples that disagree on the same state; a flow bound wider than the contract’s; a rule left only in prose. Those four are the list to walk before you call the interface done.

Before handing over, walk the brief once more against the interface: every rule of list 3 is an invariant, a bound or a machine, and has the outcome that keeps it; every failure in list 2 is declared and exampled or marked unreachable; every read of list 4 is a view; every caller condition of list 5 is inside a uses caller flow or a view; every assumption in ASSUMPTIONS.md has its comment in the interface.

What you hand over

Five files, in one directory:

The worked example

This slot is open. The example will be a conventional requirement the author is supplying (a dialer), carried from its prose through the brief and the assumptions to vishy check --interface passing, in docs/examples/authoring/, in the five files above. Until it lands, the handbook’s example is the small case every command above was run on.