Why this language

Vishy is a language for the logic of an application: what exists, what may be done to it, what must always hold, and who may do what. A program in it is a set of units, each owning some state and the rules about it; contracts that change a unit’s state and name what happened; flows that compose contracts into transactions across units; and scenarios and invariants that say what must be true. A compiler checks all of that, a verifier looks for the state that breaks a rule, and the same program can be turned into a stored, served application.

Two things are taken away, on purpose, and everything else in this book follows from them.

A unit cannot be reached into. No contract in one unit reads or writes another unit’s state. The only way in is through the unit’s own contracts, and the only things that span units are flows and world rules, both written where the compiler can see them. So a unit can be written and checked alone, a program splits into parts that different people or models write at the same time, and the compiler knows every point where two units touch.

A contract is known by what it declares, not by its body. A contract’s header names its outcomes: how it can succeed, how it can fail, what value it carries. Its examples say what happens in particular states. Everything a caller may rely on is in that header and those examples, and the verifier holds the body to them in states nobody wrote down. Writing the body is the smaller half of the work.

Each layer of computing that lasted took something away and had a machine underneath that made the removal free: the transistor let you stop caring about voltage, the compiler about registers. Here the removals are the two above and the machine is the verifier. Whether they are the right removals is what the programs in this repository are testing; the measurements are in the appendices, not in this foreword.

How to read this guide

One concept per chapter, in the order a person meets them. Every chapter has one program, under forty lines, and shows what the compiler prints for it. The programs are files in the repository (book/programs/), and a check, tests/check_book.sh, runs each one and compares the compiler’s answers with the ones printed here, so what you read is what the compiler does on the day the book was built. Most chapters end with one thing to try: remove a line and watch what the verifier finds.

The guide is written for a person learning the language, and for a model that will write in it. The reference is the authority on notation and is cited where a chapter leaves something out. Building an application with several writers, human or model, is a chapter of its own and a separate handbook; you do not need it to learn the language.