Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The shape of a program

A Vishy program is a model of a domain that the compiler can run and check. Before any syntax, hold this shape:

  • Units own facts. Each unit holds some state, rows in tables and a few scalars, and every rule about that state. Nothing outside the unit can read or change it.
  • Contracts are what may happen to a thing, and how it can refuse. Each contract names its outcomes: the ways it succeeds, the ways it fails, the value it carries. Its body says what changes.
  • Flows are the transactions that compose contracts across units: a sequence of calls that either all happen or none do. They are the only place two units meet, and a fact one unit needs from another travels through a flow as a value.
  • Views are the reads: an expression over the state, with the rule of who may see it inside the expression.
  • Rules are invariants: what must hold inside one unit after every call, and what must hold across units after every flow.
  • Nothing reaches into anything else, and the machine checks the whole: examples, scenarios, sampled calls from random states, walks of the flows, every rule after every step.

If you have built software with domain-driven design, these are the names you know with the boundaries enforced: a unit is an aggregate, a contract a command with its invariant, a flow an application service, a view a read model, emitted events and the outbox the domain events, a migration a migration. The difference is that here the aggregate boundary is a compile error, not a convention: a contract that reads another unit does not compile. The guide uses those names where they fit.

If you come from elsewhere, three short pages map the shape onto what you know, each with the first program you would write: SQL, Elm and Redux, and domain-driven design in more detail. Readers of formal methods need no page: scenarios are traces, invariants are invariants, and the sampled checks are small-scope checking that runs. Readers of Rust are the easiest to mislead, which is why this guide never borrows Rust’s shape; the one mapping that holds is ownership of state for ownership of memory.

The rest of the guide takes the shape one piece at a time: first everything inside one unit, then many units, then many writers, then the world outside the program.