Where the tests went

In most codebases the test code outweighs the code. This page says why that is, what Vishy does about it, and, honestly, what it does not.

Why tests outweigh code

An ordinary compiler proves types and nothing about meaning. It knows that withdraw takes a number and returns a result; it does not know that the balance may not go negative. So every fact about behaviour has to be stated somewhere else, as a hand-written test: one point in the state space per fact, and one more per bug ever found. The suite is the specification, written by enumeration, and enumeration never finishes: the test that would have caught the next bug is the one nobody thought to write.

The compiler that builds Vishy has this disease in the mild form of a careful project. Its source is 8331 lines of Rust and its checks are 3331 lines of scripts and programs, two fifths as much again, and every one of those checks is a point somebody chose. That is one honest reason the roadmap ends at a compiler written in Vishy.

What Vishy does about it

The specification is not reduced. It is moved, from the place where it decays into the place the compiler reads it.

• An example is one artifact with three jobs. { balance: 100 } (200) => Insufficient; is the writer’s specification of the contract, the checker’s acceptance test of the body, and the rule’s documentation, in one line that the compiler runs. In a suite those are three files that drift apart.
• The number of examples is fixed by the interface, not by fear. Every declared outcome needs one example that produces it, and the checker refuses an interface without. Nobody decides how many tests are enough; the outcomes decide.
• The sampled checks generate what a suite approximates by hand. A thousand random states and arguments per contract, from random and from reached states, with every rule checked after each call, is the test nobody could enumerate. An invariant is a test over every state the verifier reaches, written once.
• Scenarios are the behavioural tests that remain, and they are few, because they say what the product does, not what each function returns.

On the tracker, an issue tracker of nine units, the interface is 1123 lines, of which 357 are inside examples and scenario blocks: about a third. The other two thirds are the rows, the contract headers with their outcomes and rules, and the flows: the specification’s other half, which a suite does not hold at all.

The measurement

Twelve bugs were planted by hand in the tracker’s contract bodies, each a realistic writer’s mistake: a bound off by one, a dropped guard, a flipped comparison, a status forgotten in a condition (experiments/research/mutation-study.md). All twelve were caught. Ten of them died deterministically, independent of how much the verifier sampled: nine on an example the interface author had written, one on the checker’s rule that a declared outcome must be produced by some case. One died on a scenario. One needed the sampler to reach a particular world, and did at 3,000 iterations but not at 300. The specification in the interface is what killed, not the size of the sample.

The same tracker was built the conventional way by the same cheap writers from the same brief (apps/COMPARISON.md). That arm’s verification is 151 scripted steps, and nothing else: no rule checked in any state those steps do not visit.

What no language can do

What no language can do is remove the need to say what the program should do. The ones that claim to are hiding the tests somewhere. Vishy asks for the saying up front, in the interface, in a form the compiler can run against states nobody wrote down; the cost is that the interface has to be right, which is the subject of the authoring guide in the appendices.