What Vishy is not

If you have written Rust, TypeScript or Python, your hands know constructs that Vishy does not have, and the compiler will refuse them. This page is those refusals, each as a program a reader from another language would write and the compiler’s answer, so that the habits are unlearned before the guide begins. Read it twice if you are a model: every construct below was tried by a model in the experiments that shaped the language.

Vishy has two layers, and the refusals on this page are the first layer’s. The core, where applications live, is closed on purpose: every value bounded, no recursion, no unbounded loop, every rule checkable, and that is what lets the verifier know everything about a program. General computation exists, behind a declared boundary called the sealed layer: recursion, while, return, unbounded text and lists, rows that contain themselves. Vishy’s own lexer and parser are written in it today, and the compiler is heading there. So each refusal below reads “the core refuses”, never “the language cannot”; the last section shows the boundary.

What Vishy is not is a scripting language: no console, no print statement, no top-to-bottom run. A program is state and rules, and it is run by calling it.

The core has no `while`

unit Counter {
    state n: int = 0;
    contract bump_to(k: int(1, 10)) => Done: n := count_up(n, k);
}
fn count_up(n: int, k: int) -> int { var i = n; while i < k { i := i + 1; } i }

book/refusals/loop.vish:5:49: error: `while` belongs to a `sealed fn`; a core function's loops are bounded (`repeat n { … }`)
  fn count_up(n: int, k: int) -> int { var i = n; while i < k { i := i + 1; } i }
                                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^

A core function is total: it always finishes. Loops are repeat n { … } with a bound, and most of what a loop would do is a quantifier over a table (count, all, any, where, fold), which the chapter on reading state shows. A while is written in a sealed function, below.

The core has no recursion

unit Counter {
    state n: int = 0;
    contract set(k: int(0, 10)) => Done: n := fact(k);
}
fn fact(k: int) -> int = if k <= 1 then 1 else k * fact(k - 1);

book/refusals/recursion.vish:5:4: error: `fact` calls itself; a core function is total, recursion belongs to a `sealed fn`
  fn fact(k: int) -> int = if k <= 1 then 1 else k * fact(k - 1);
     ^^^^

The core has no `return`

unit Counter {
    state n: int = 0;
    contract read() -> int { else => Value(n); }
}
fn pick(a: int, b: int) -> int { if a > b { return a; } b }

book/refusals/return.vish:5:45: error: `return` belongs to a `sealed fn`; a core function's block ends with its result expression
  fn pick(a: int, b: int) -> int { if a > b { return a; } b }
                                              ^^^^^^^^^

A block ends with its result. if is an expression: if a > b then a else b.

There is no assignment; there are deltas

unit Counter {
    state n: int = 0;
    contract bump() { else => Done: n = n + 1; }
}

book/refusals/mutation.vish:3:39: error: expected `:=`, `+=`, `-=`, `max=` or `min=` in delta, found `=`
      contract bump() { else => Done: n = n + 1; }
                                        ^

A contract does not run statements. It names what changes, as deltas: n += 1, n := 0, t += [row], t[k].f := e. Everything not named is unchanged, and every right-hand side reads the state before the call. = is not an operator in a delta, and there is no variable to assign to.

There is no `for`; there are set-valued deltas

row Item { id: id, n: int }
unit Items {
    state items: Item[8];
    contract bump_all() => Done: for x in items { items[x.id].n += 1; };
}

book/refusals/forloop.vish:4:38: error: expected `:=`, `+=`, `-=`, `max=` or `min=` in delta, found `x`
      contract bump_all() => Done: for x in items { items[x.id].n += 1; };
                                       ^

Changing every row, or every row that matches, is one delta: items.n += 1, or items.n := for x where x.n > 3 => 0. A loop that walks a table and changes rows one by one is not written in this language.

There are no structs, classes, traits or interfaces in that sense

struct Point { x: int, y: int }
unit Points {
    state p: Point;
    contract origin() => Done: p := Point { x: 0, y: 0 };
}

book/refusals/struct.vish:1:1: error: expected `unit`, `flow`, `view`, `row`, `events`, `fn`, `invariant`, `derived`, `scenario`, `route`, `deliver`, `version` or `migrate`, found `struct`
  struct Point { x: int, y: int }
  ^^^^^^

The compiler’s answer lists everything a program may declare at the top level. A record type is a row. There are no methods on rows, no inheritance, no generics of your own; the word “interface” in this guide means a program whose contracts are declared but not yet written, which is a later chapter.

A unit cannot read another unit

unit Rooms {
    state open: bool = true;
    contract close() => Closed: open := false;
}
unit Bookings {
    state count: int = 0;
    contract book() {
        case !Rooms.open => fail RoomClosed;
        else => Booked: count += 1;
    }
}

book/refusals/reach.vish:8:15: error: unknown name `Rooms`
          case !Rooms.open => fail RoomClosed;
                ^^^^^

Inside Bookings, the name Rooms does not exist. This is the language’s first removal, and it is not a visibility setting that could be opened: there is no pub, no import that would allow it. A fact that Bookings needs from Rooms is carried in by a flow, as a value, which the flows chapter shows.

A contract cannot call a contract

unit Rooms {
    state open: bool = true;
    contract close() => Closed: open := false;
}
unit Bookings {
    state count: int = 0;
    contract book_and_close() => Booked: count += 1, Rooms.close();
}

book/refusals/call.vish:7:65: error: expected `:=`, `+=` or `-=` in delta, found `(`
      contract book_and_close() => Booked: count += 1, Rooms.close();
                                                                  ^

A contract’s body is cases and deltas, nothing else: no calls, no effects, no clock. Composition happens in flows, which call contracts in sequence as one transaction.

What else is missing, by design

No floating-point numbers; money and time are integers with a scale.
No null; an absent value is option<T>, read with match.
No exceptions; a failure is a named outcome, fail Insufficient, and it changes nothing.
No pointers, references, borrowing or lifetimes; there is nothing to point at.
No input or output from the program itself; the world enters through declared effects and leaves through outcomes, events and views.
No user interface; a served program answers JSON at routes, and the screen is someone else’s program.

The compiler accepts an unbounded int or string, and the guide will ask you never to write one in a program that matters, for reasons the chapter on values gives.

What exists behind the boundary

The same three constructs, accepted, because they are declared sealed:

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 }
examples total { (Node { v: 1, kids: [Node { v: 2, kids: [] }, Node { v: 3, kids: [] }] }) => 6; }
examples count_to { (0) => 0; (7) => 7; }
unit Counter {
    state n: int = 0;
    contract set(k: int(0, 100)) => Set: n := count_to(k);
}
scenario s { Counter.set(7) => Set; }

verify: 3 examples, 1 scenario steps and 2000 sampled checks passed

A sealed function may recurse, loop with while, return early, and take and return text and lists without a bound; a sealed row may contain itself. What the seal promises: the function is pure, it has no state and no effects, and its result is trusted only to its declared type, which the boundary checks. What it does not promise: that it finishes; so a sealed function is tested by its examples and by every call the core makes to it, under a step budget, and is never sampled on its own. The core calls it as it calls any function, and the core stays closed. The chapter on functions says the rest, and the reference (§7) is the authority.

Readers from Rust will want to map the seal onto unsafe. That is the wrong row. Three kinds of code exist in a program, and the trust the compiler gives each is different:

code	what checks it	what it may do
the core: units, contracts, flows, views	the verifier: examples, scenarios, sampled checks, every rule	applications
sealed functions	their examples, a step budget, the declared type at the boundary	general computation: recursion, loops, trees, text; pure, no unit state, no events, no effects; the result cannot corrupt the core
effects with a Rust body	nothing; trusted	anything: the outside world, crates, input and output

The seal gives up totality and sampling and keeps everything else, so a sealed function is tested, not proven, and never unsafe. Vishy’s unsafe is an effect’s Rust body, where the checker trusts you completely (reference §18).

Everything Vishy does have is in the chapters that follow. When a construct you expect is missing, the answer is almost always one of: a quantifier, a delta, a flow, or an outcome.

Keyboard shortcuts

The Vishy Guide