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

Your first program

The compiler

The compiler is one program, vishy, built from the repository with Cargo:

cargo build

The binary is target/debug/vishy. Every command in this book is run from the repository root, and vishy in the text means that path. Three commands are all a learner needs:

commandwhat it answers
vishy check <file>Does the program make sense? Types, names, examples, and a count of what it declares.
vishy run <file>What do the scenarios do? Each step’s outcome, then each unit’s state.
vishy verify <file> [seed] [iterations]Does every rule hold? Examples, scenarios, then thousands of sampled calls from random states.

The smallest program

Other languages begin with a program that prints “hello, world”. A Vishy program prints nothing, ever: it has no output statement, no console, no strings to write. What it has is state and outcomes. A program is run by calling its contracts, and what comes back is the outcome of each call and the state afterwards. So the smallest program is a unit with a little state, two contracts, and a scenario that calls them and says what must come back:

unit Counter {
    state n: int = 0;
    contract bump() => Ok: n += 1;
    contract read() -> int => Value(n);
}
scenario hello {
    Counter.bump() => Ok;
    Counter.bump() => Ok;
    Counter.read() => Value(2);
}

Read it in words. There is one unit, Counter, which owns one number, n, starting at zero. It has two contracts. bump succeeds with the outcome Ok and adds one to n. read succeeds with the outcome Value and carries the current n with it, which is why its header says it returns an int. The scenario hello is a script: call bump twice, then read, and each line says which outcome must come back.

vishy check book/programs/hello.vish prints:

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

Two flows, though the program declares none: a scenario step that calls a contract directly is a one-call flow the compiler makes for it. Flows are the subject of a later chapter; for now, every call from outside a unit goes through one.

vishy run book/programs/hello.vish runs the scenario and prints the trace and the final state. This trace is the program’s output; there is no other:

scenario hello
  Counter.bump() => Ok
  Counter.bump() => Ok
  Counter.read() => Value(2)
  Counter = Counter { n: 2 }
3 step(s), all as expected

vishy verify book/programs/hello.vish 7 1000 runs the scenario too, then calls bump and read from sampled states, four thousand calls in all, and checks that nothing goes wrong. There are no rules in this program yet, so “nothing goes wrong” means no call failed in a way the program did not declare:

verify: 0 examples, 3 scenario steps and 4000 sampled checks passed

The two numbers after the file name are the random seed and the number of iterations. The same seed gives the same sampled states every time, so a failure can be reproduced by anyone with the same file.

The playground

sh playground/run.sh builds a small web page that runs these three commands on a program you paste in, at http://127.0.0.1:8080. The page is itself a Vishy program served the way the last chapters describe.

The answer comes back

So where is “hello, world”? In Vishy it is an answer, not a printed line. A contract can carry text as its value; a flow calls the contract; a route names the flow; and a served program answers a call with that value:

unit Greeter {
    caps storage;
    state greeted: int = 0;
    contract greet() -> string(16) => Greeting("hello, world"): greeted += 1;
}
flow greet() atomic { Greeter.greet(); }
route POST "/hello" => greet();
scenario once {
    greet() => Greeting("hello, world");
}

vishy run shows the scenario receiving the greeting:

scenario once
  greet() => Greeting("hello, world")
  Greeter = Greeter { greeted: 1 }
1 step(s), all as expected

And vishy service book/programs/greeting.vish out sqlite writes a small server that, built and started (the chapter on storage and the door shows the three commands), answers the route:

POST /hello
{"events":[],"ok":true,"outcome":"Greeting","value":"hello, world"}

ok says the flow succeeded, outcome is the name the contract answered with, and value is what it carried. That JSON line is the guide’s hello world, and the check that keeps this guide true starts that server and makes the call every time it runs.

Why there is no print statement: printing is a side effect, and the verifier cannot check what leaves the program that way. So every way out of a Vishy program goes through a declared boundary the compiler can see: the answer to a call, a view, a delivery, an effect. What a program says is always something a caller receives.

Try

Change Value(2) to Value(3) and run vishy run again. The trace stops at the step that disagreed and shows the state at that moment. That is the shape of every failure the tools report: the step or the call, what was expected, what happened, and the state.