Building with a team

On a real project today, a dialer platform, one agent has to do QA on the softphone while another integrates something into the frontend. Two agents, two features, one codebase. Agents struggle badly with that level of parallelism in any ordinary language: not because they are weak at either task, but because of what the codebase does not say. This appendix is about that, and about the part of it Vishy changes. It ends with the team handbook’s substance: the roles, the sequence on the room-booking program, and what to do when a step fails.

Why it is structural

The trouble is not a prompting problem. It comes from four facts about an ordinary codebase, and no instruction to either agent removes them.

• Nothing says who owns what. Two agents on different features touch the same tables, the same handlers, the same helpers, because nothing in the code marks a table as one feature’s. Each edit is legal; the pair is not.
• The only arbiter is the whole test suite. It is slow, it is shared, and its answer is “something broke”. It does not say whose change broke it, so both agents read the failure, both suspect the other, and one of them re-runs everything to find out.
• The contract between frontend and backend lives in prose and in heads. The frontend agent builds against an integration that is still moving, guesses at the shape of an answer, and finds out at the end whether the guess held.
• Coordination is done by reading each other’s diffs. That is the thing agents do worst: a diff is a list of edits without the intent that made them, and reconciling two of them is the work the whole arrangement was meant to avoid.

What the language changes

On the part of the system the core covers, the state and its rules, the language takes each of the four facts away.

• State has one owner, and the language refuses a second writer. A unit’s state is changed only by that unit’s contracts; another unit cannot name it, and the checker says so (What Vishy is not shows the refusal). Two agents on two units cannot touch the same table, because there is no way to write it from outside.
• The interface is fixed first, with examples, and a writer gets a local verdict in under a second with nobody else’s work present. The interface owner writes every row, every rule, every contract’s outcomes and examples, before any body exists. A unit’s writer then receives only the shared declarations and their own unit, writes the bodies, and checks them alone: the examples, the interface’s examples, and sampled calls against the unit’s own invariant. The verdict names the contract, the state and the arguments. Nothing another writer is doing is in that check.
• Assembly is the one shared step, and the verifier decides, not a reviewer. When every part passes, the whole program is checked and verified: every example, every scenario, the walks over the flows, the world rules. A part is accepted when its local check passes; a program is accepted when the verifier passes. No review replaces either, and no review is asked to.
• A verdict names its contract, and the routing is written down. A failure that names a contract goes to that unit’s writer; a failure on a world rule or a scenario goes to the interface owner first, who decides whether the rule, the flow or a body is wrong. The Process page of the anti-patterns part says which verdicts that name a contract are the interface’s fault, and how to tell.
• The wire contract is generated from the interface, so a frontend agent builds against a door that does not move. The routes, the request bodies with their bounds, the outcomes a client switches on and the typed clients all come from the interface file, before any body is written (the wire contract is that page). The frontend agent’s guess is replaced by a generated file, and an interface change is a new version of that file, diffed, not a surprise.

What it does not change

Said plainly: the softphone QA is audio, WebRTC and screens, and the frontend integration is host-side code. Both sit outside the core, in the world the three-kinds-of-code table puts under “effects” and beyond, and the parallelism problem stays hard there for everyone, this language included. What the language gives those two agents is narrower than a solution and still real: a fixed contract to build against, and a backend whose rules are already verified. The QA agent tests the phone, instead of rediscovering rule bugs through it.

The roles

One application has one interface owner and any number of unit owners.

• The interface owner writes the brief and the interface: rows, enums, events, every unit’s state, fixtures, invariants and stub contracts with examples, the flows, views, routes, world rules, scenarios, deliveries, migrations. The interface is the only shared file. Nobody else edits it; a unit owner who needs a change asks for it.
• A unit owner writes the contract bodies of one unit, as a part, and nothing else. The writer stage, vishy write, can be that owner: a cheap model behind the same checks. A person or a stronger agent takes a unit the stage cannot finish.
• The verifier decides. A part is accepted when its local check passes; a program is accepted when vishy verify passes at three thousand iterations.

The split works because a unit cannot be reached into. Nothing outside a unit reads its state, so a unit’s body can be written and checked alone, and the interface is the whole of what its writer needs.

The sequence

The example is the guide’s room-booking program: two units, six contracts, four flows, two views, six routes, one scenario. Every line the tools print below is regenerated by the guide’s check; the timings are the team handbook’s, from its run on a laptop, and are named as such.

1. The brief

A page of prose: what exists, the rules, who may do what, the screens. For the rooms it is six lines: a room has a name and seats and can be closed, and closing it cancels its bookings; a booking is one room, one day, one slot, for some people, held by whoever made it; rule 1, a booking’s room exists, is open and seats at least the booking’s people; rule 2, a room has at most one booking per day and slot; only the holder cancels; two screens, my bookings and a room’s day. Number the rules; the interface cites them. The appendix on authoring an interface says how to get from any requirement to this page.

2. The interface

The owner writes it against the checker until it passes:

row Room { id: id, name: string(64), seats: int(1, 200), closed: bool }
row Booking { id: id, room: id, holder: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200) }

// rule 1: a booking's room exists, is open, and seats at least the booking's people.
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && !r.closed && b.people <= r.seats));

unit Rooms {
    caps storage;
    state rooms: Room[32];
    fixture Two = { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }, Room { id: 2, name: "Beta", seats: 10, closed: true }] };
    contract add(room: id, name: string(64), seats: int(1, 200)) {
        // Exists when the room id is present; else insert Room { id: room, name, seats, closed: false }.
        outcomes Added, fail Exists;
        examples {
            {} (1, "Alpha", 4) => Added { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }] };
            Two (1, "Again", 3) => Exists;
        }
    }
    contract fits(room: id, people: int(1, 200)) {
        // Fits when the room exists, is open and has at least `people` seats; RoomClosed when it is closed; TooSmall when open with fewer seats; an absent room is Unknown. Changes nothing.
        outcomes Fits, fail RoomClosed, fail TooSmall;
        examples {
            Two (1, 4) => Fits;
            Two (1, 5) => TooSmall;
            Two (2, 1) => RoomClosed;
            Two (9, 1) => Unknown;
        }
    }
    contract close(room: id) {
        // Closed: the room's closed becomes true (already closed is fine); an absent room is Unknown.
        outcomes Closed;
        examples {
            Two (1) => Closed { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: true }, Room { id: 2, name: "Beta", seats: 10, closed: true }] };
            Two (2) => Closed;
            Two (9) => Unknown;
        }
    }
}

unit Bookings {
    caps storage;
    state bookings: Booking[64];
    fixture One = { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }] };
    // rule 2: one booking per room, day and slot.
    invariant all(a in bookings: all(b in bookings: a.id == b.id || a.room != b.room || a.day != b.day || a.slot != b.slot));
    contract book(booking: id, room: id, holder: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200)) {
        // Exists when the booking id is present; Taken when the room already has a booking on that day and slot; else insert Booking { id: booking, room, holder, day, slot, people }.
        outcomes Booked, fail Taken, fail Exists;
        examples {
            {} (1, 1, 100, 10, 2, 3) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }] };
            One (1, 2, 100, 11, 1, 1) => Exists;
            One (2, 1, 101, 10, 2, 1) => Taken;
            One (2, 1, 101, 10, 3, 1) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }, Booking { id: 2, room: 1, holder: 101, day: 10, slot: 3, people: 1 }] };
        }
    }
    contract cancel(booking: id, holder: id) {
        // Cancelled: removes the booking when its holder is `holder`; NotHolder when it is someone else's; an absent booking is Unknown.
        outcomes Cancelled, fail NotHolder;
        examples {
            One (1, 100) => Cancelled { bookings: [] };
            One (1, 101) => NotHolder;
            One (9, 100) => Unknown;
        }
    }
    contract clear_room(room: id) {
        // Cleared: removes every booking of the room (none is fine).
        outcomes Cleared;
        examples {
            One (1) => Cleared { bookings: [] };
            One (2) => Cleared;
        }
    }
}

flow add_room(room: id, name: string(64), seats: int(1, 200)) atomic { Rooms.add(room, name, seats); }
// rule 1 is kept: the bookings go before the room closes.
flow close_room(room: id) atomic { Bookings.clear_room(room); Rooms.close(room); }
// rule 1 is kept: the room decides whether the booking fits before it is made.
flow book(booking: id, room: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200)) uses caller atomic { Rooms.fits(room, people); Bookings.book(booking, room, caller, day, slot, people); }
flow cancel(booking: id) uses caller atomic { Bookings.cancel(booking, caller); }

view my_bookings() uses caller = where(b in Bookings.bookings: b.holder == caller);
view room_day(room: id, day: int(1, 366)) = where(b in Bookings.bookings: b.room == room && b.day == day);

route POST "/rooms" => add_room(room, name, seats);
route POST "/rooms/{room}/close" => close_room(room);
route POST "/bookings" => book(booking, room, day, slot, people);
route POST "/bookings/{booking}/cancel" => cancel(booking);
route GET "/me/bookings" => my_bookings();
route GET "/rooms/{room}/days/{day}" => room_day(room, day);

scenario a_day_in_alpha {
    add_room(1, "Alpha", 4) => Added; add_room(1, "Again", 2) => Exists; add_room(2, "Beta", 10) => Added;
    as 100 book(1, 1, 10, 2, 3) => Booked;
    as 101 book(2, 1, 10, 2, 1) => Taken;
    as 101 book(2, 1, 10, 3, 5) => TooSmall;
    as 101 book(2, 9, 10, 3, 1) => Unknown;
    as 101 cancel(1) => NotHolder;
    as 100 my_bookings() => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }]);
    room_day(1, 10) => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }]);
    close_room(1) => Closed;
    as 100 my_bookings() => Value([]);
    as 102 book(3, 1, 11, 1, 1) => RoomClosed;
    as 100 cancel(1) => Unknown;
}

vishy check --interface team-rooms.vish

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

Every contract is a stub: outcomes declared, examples given, no cases. The check refuses a contract with a body, a declared failure without an example, a flow passing the wrong type to a stub, an outcome name used with two shapes, a scenario step that cannot type. The Contract page of the anti-patterns part shows each refusal. The four rules that cost the most when skipped: bound every quantity; every failure a rule implies is an outcome of some contract, with an example that produces it; a rule that couples two 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); a fact one unit needs from another is carried by the flow as a value (book asks Rooms.fits first), never read across.

3. The parts

vishy write team-rooms.vish --out parts

One request per unit, all at once; each part is checked as it lands; the contracts a check names are retried; then assembly and verification. The team handbook’s run on this example: both units answered in 2.9 seconds, 6.2 seconds in all with verification; a second run kept every part that still passed and wrote nothing, in 0.6 seconds. After an interface change, only the contracts the change reaches are rewritten.

A unit the stage cannot finish goes to a person or a stronger agent, who asks for the brief and writes the part by hand:

vishy brief team-rooms.vish Rooms
vishy part team-rooms.vish Rooms parts/rooms.vish

The brief prints the writer’s reference, the shared declarations with their comments, the world rules that name the unit, and the unit’s block as the owner wrote it; nothing about the other units. The part check is the same local check the stage runs. The guide’s check runs it on this example’s rooms part against the interface:

verify: 21 examples, 0 scenario steps and 1500 sampled checks passed

It leaves out flows, scenarios, world rules and views, which belong to the whole program.

4. Assembly and verification

The interface and the two parts, assembled into one program:

row Room { id: id, name: string(64), seats: int(1, 200), closed: bool }
row Booking { id: id, room: id, holder: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200) }

// rule 1: a booking's room exists, is open, and seats at least the booking's people.
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && !r.closed && b.people <= r.seats));

unit Rooms {
    caps storage;
    state rooms: Room[32];
    fixture Two = { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }, Room { id: 2, name: "Beta", seats: 10, closed: true }] };
    contract add(room: id, name: string(64), seats: int(1, 200)) {
        // Exists when the room id is present; else insert Room { id: room, name, seats, closed: false }.
        outcomes Added, fail Exists;
        examples {
            {} (1, "Alpha", 4) => Added { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }] };
            Two (1, "Again", 3) => Exists;
        }
    }
    contract fits(room: id, people: int(1, 200)) {
        // Fits when the room exists, is open and has at least `people` seats; RoomClosed when it is closed; TooSmall when open with fewer seats; an absent room is Unknown. Changes nothing.
        outcomes Fits, fail RoomClosed, fail TooSmall;
        examples {
            Two (1, 4) => Fits;
            Two (1, 5) => TooSmall;
            Two (2, 1) => RoomClosed;
            Two (9, 1) => Unknown;
        }
    }
    contract close(room: id) {
        // Closed: the room's closed becomes true (already closed is fine); an absent room is Unknown.
        outcomes Closed;
        examples {
            Two (1) => Closed { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: true }, Room { id: 2, name: "Beta", seats: 10, closed: true }] };
            Two (2) => Closed;
            Two (9) => Unknown;
        }
    }
}

unit Bookings {
    caps storage;
    state bookings: Booking[64];
    fixture One = { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }] };
    // rule 2: one booking per room, day and slot.
    invariant all(a in bookings: all(b in bookings: a.id == b.id || a.room != b.room || a.day != b.day || a.slot != b.slot));
    contract book(booking: id, room: id, holder: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200)) {
        // Exists when the booking id is present; Taken when the room already has a booking on that day and slot; else insert Booking { id: booking, room, holder, day, slot, people }.
        outcomes Booked, fail Taken, fail Exists;
        examples {
            {} (1, 1, 100, 10, 2, 3) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }] };
            One (1, 2, 100, 11, 1, 1) => Exists;
            One (2, 1, 101, 10, 2, 1) => Taken;
            One (2, 1, 101, 10, 3, 1) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }, Booking { id: 2, room: 1, holder: 101, day: 10, slot: 3, people: 1 }] };
        }
    }
    contract cancel(booking: id, holder: id) {
        // Cancelled: removes the booking when its holder is `holder`; NotHolder when it is someone else's; an absent booking is Unknown.
        outcomes Cancelled, fail NotHolder;
        examples {
            One (1, 100) => Cancelled { bookings: [] };
            One (1, 101) => NotHolder;
            One (9, 100) => Unknown;
        }
    }
    contract clear_room(room: id) {
        // Cleared: removes every booking of the room (none is fine).
        outcomes Cleared;
        examples {
            One (1) => Cleared { bookings: [] };
            One (2) => Cleared;
        }
    }
}

flow add_room(room: id, name: string(64), seats: int(1, 200)) atomic { Rooms.add(room, name, seats); }
// rule 1 is kept: the bookings go before the room closes.
flow close_room(room: id) atomic { Bookings.clear_room(room); Rooms.close(room); }
// rule 1 is kept: the room decides whether the booking fits before it is made.
flow book(booking: id, room: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200)) uses caller atomic { Rooms.fits(room, people); Bookings.book(booking, room, caller, day, slot, people); }
flow cancel(booking: id) uses caller atomic { Bookings.cancel(booking, caller); }

view my_bookings() uses caller = where(b in Bookings.bookings: b.holder == caller);
view room_day(room: id, day: int(1, 366)) = where(b in Bookings.bookings: b.room == room && b.day == day);

route POST "/rooms" => add_room(room, name, seats);
route POST "/rooms/{room}/close" => close_room(room);
route POST "/bookings" => book(booking, room, day, slot, people);
route POST "/bookings/{booking}/cancel" => cancel(booking);
route GET "/me/bookings" => my_bookings();
route GET "/rooms/{room}/days/{day}" => room_day(room, day);

scenario a_day_in_alpha {
    add_room(1, "Alpha", 4) => Added; add_room(1, "Again", 2) => Exists; add_room(2, "Beta", 10) => Added;
    as 100 book(1, 1, 10, 2, 3) => Booked;
    as 101 book(2, 1, 10, 2, 1) => Taken;
    as 101 book(2, 1, 10, 3, 5) => TooSmall;
    as 101 book(2, 9, 10, 3, 1) => Unknown;
    as 101 cancel(1) => NotHolder;
    as 100 my_bookings() => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }]);
    room_day(1, 10) => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }]);
    close_room(1) => Closed;
    as 100 my_bookings() => Value([]);
    as 102 book(3, 1, 11, 1, 1) => RoomClosed;
    as 100 cancel(1) => Unknown;
}

unit Rooms {
contract add(room: id, name: string(64), seats: int(1, 200)) {
    case room in rooms => fail Exists;
    else => Added: rooms += [Room { id: room, name: name, seats: seats, closed: false }];
    examples {
        {} (1, "Alpha", 4) => Added { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }] };
        Two (1, "Again", 3) => Exists;
        Two (3, "Gamma", 6) => Added { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: false }, Room { id: 2, name: "Beta", seats: 10, closed: true }, Room { id: 3, name: "Gamma", seats: 6, closed: false }] };
    }
}
contract fits(room: id, people: int(1, 200)) {
    case !(room in rooms) => fail Unknown;
    case rooms[room].closed => fail RoomClosed;
    case people > rooms[room].seats => fail TooSmall;
    else => Fits;
    examples {
        Two (1, 4) => Fits;
        Two (1, 5) => TooSmall;
        Two (2, 1) => RoomClosed;
        Two (9, 1) => Unknown;
        {} (1, 1) => Unknown;
    }
}
contract close(room: id) {
    case !(room in rooms) => fail Unknown;
    else => Closed: rooms[room].closed := true;
    examples {
        Two (1) => Closed { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: true }, Room { id: 2, name: "Beta", seats: 10, closed: true }] };
        Two (2) => Closed;
        Two (9) => Unknown;
        {} (1) => Unknown;
    }
}
}

unit Bookings {
contract book(booking: id, room: id, holder: id, day: int(1, 366), slot: int(1, 8), people: int(1, 200)) {
    case any(b in bookings: b.id == booking) => fail Exists;
    case any(b in bookings: b.room == room && b.day == day && b.slot == slot) => fail Taken;
    else => Booked: bookings += [Booking { id: booking, room: room, holder: holder, day: day, slot: slot, people: people }];
    examples {
        {} (1, 1, 100, 10, 2, 3) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }] };
        One (1, 2, 100, 11, 1, 1) => Exists;
        One (2, 1, 101, 10, 2, 1) => Taken;
        One (2, 1, 101, 10, 3, 1) => Booked { bookings: [Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }, Booking { id: 2, room: 1, holder: 101, day: 10, slot: 3, people: 1 }] };
    }
}
contract cancel(booking: id, holder: id) {
    case any(b in bookings: b.id == booking && b.holder == holder) => Cancelled: bookings -= [booking];
    case any(b in bookings: b.id == booking) => fail NotHolder;
    else => fail Unknown;
    examples {
        One (1, 100) => Cancelled { bookings: [] };
        One (1, 101) => NotHolder;
        One (9, 100) => Unknown;
    }
}
contract clear_room(room: id) {
    else => Cleared: bookings -= where(b in bookings: b.room == room).id;
    examples {
        One (1) => Cleared { bookings: [] };
        One (2) => Cleared;
    }
}
}

vishy run team-rooms.vish
vishy verify team-rooms.vish 7 1000

scenario a_day_in_alpha
  add_room(1, "Alpha", 4) => Added
  add_room(1, "Again", 2) => Exists
  add_room(2, "Beta", 10) => Added
  book(1, 1, 10, 2, 3) => Booked
  book(2, 1, 10, 2, 1) => Taken
  book(2, 1, 10, 3, 5) => TooSmall
  book(2, 9, 10, 3, 1) => Unknown
  cancel(1) => NotHolder
  my_bookings() => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }])
  room_day(1, 10) => Value([Booking { id: 1, room: 1, holder: 100, day: 10, slot: 2, people: 3 }])
  close_room(1) => Closed
  my_bookings() => Value([])
  book(3, 1, 11, 1, 1) => RoomClosed
  cancel(1) => Unknown
  Rooms = Rooms { rooms: [Room { id: 1, name: "Alpha", seats: 4, closed: true }, Room { id: 2, name: "Beta", seats: 10, closed: false }] }
  Bookings = Bookings { bookings: [] }
14 step(s), all as expected

verify: 39 examples, 14 scenario steps and 12000 sampled checks passed

The scenario is the brief’s day in room Alpha, every failure reached through a flow. Run it on three seeds and at three thousand iterations before serving anything; the guide’s check runs one seed at one thousand, which is the line above. A failure names the flow or the contract, the world and the arguments.

5. The service and the clients

vishy service team-rooms.vish out/service sqlite
vishy client  team-rooms.vish out/client

The first writes a Rust crate that runs each flow as a transaction over a store; the second writes a TypeScript client, an OpenAPI description and a Rust client. The guide’s check builds the service and calls its first route with an empty body; the door answers with the flow and the parameter it is missing:

POST /rooms
{"error":"missing `room`","flow":"add_room"}

That answer is the frontend agent’s contract: every parameter, every bound, every outcome, before a body exists.

When a step fails

Changing a running application

An interface change is a version of the program. The owner edits the interface, runs the interface check, then the writer stage again: parts that still pass are kept, the contracts the change reaches are rewritten. When a row changes, the program gets a version number and, for a rename or a recomputed field, a migration with an example; the chapter on versions and migrations says what the compiler derives and what it refuses. The interface diff says whether clients written against the old interface still fit.

What is not here, by decision: nothing generates a user interface. A screen is the application’s work, built on the generated clients, in whatever the team likes.

The team that built this

This guide was written by a team of agents, one chat per seat, each with a charter: the files it owns and nobody else writes, its inputs, a local check it runs before it reports, and a report in a fixed shape that someone else reproduces by running the same commands. A seat that needed a change in another seat’s file proposed the text and waited. The checks were the arbiter, and a verdict named the seat.

That is the language’s discipline done by hand: one owner per piece of state, a fixed contract between owners, a local verdict before the shared step, and a check that decides instead of a reader. It worked for the agents for the same reason it works in the language. The parallelism was never the hard part; the ownership was.