You hire a contractor to renovate your kitchen. Before work starts, you agree on the terms: the budget is $3,000 and the plumbing has to pass inspection. Those terms are the contract. If the contractor tears out a wall and finds rot, the budget might change, but the contract makes the change explicit. No $5,000 bill by surprise.

Software has the same problem. A function accepts certain inputs and promises certain outputs, but those promises usually live in the programmer's head or in a comment that falls out of date. When the function changes, nothing enforces the old promises. Bugs happen in the gap between what a function used to guarantee and what it actually does now.

Contracts make those promises explicit, and the machine checks them for you.

## What contracts look like in Vary

Vary has three kinds of contracts, each written as a block at the top of a function body.

### Preconditions: what you require from callers

A precondition says "do not call me unless these things are true." If a caller breaks this rule, the program fails immediately with a clear error instead of producing a wrong answer silently.

```vary
def divide(a: Int, b: Int) -> Int {
    in {
        b != 0
    }
    return a // b
}
```

That `in {}` block runs before the function body. If `b` is zero, you get a `ContractViolation` error pointing at the exact condition that failed. No division by zero. No mysterious `Infinity` return value that corrupts data downstream.

You can check multiple conditions:

```vary
def clamp(x: Int, lo: Int, hi: Int) -> Int {
    in {
        lo <= hi
        hi - lo > 0
    }
    if x < lo { return lo }
    if x > hi { return hi }
    return x
}
```

Each condition is checked independently. If `lo > hi`, you find out before the function does anything at all.

### Return postconditions: what you promise about the result

An `out(r) {}` block names the return value and checks conditions about it after the function finishes:

```vary
def abs_val(x: Int) -> Int {
    out(r) {
        r >= 0
    }
    if x < 0 {
        return -x
    }
    return x
}
```

Every `return` path goes through the `out` check. If any code path accidentally returns a negative number, the contract catches it. This is not a test you run separately. It is baked into the function itself.

### State postconditions: what changed and how

For functions that modify state (like methods on a class), `post {}` checks conditions after the body runs. Combined with `old()`, which snapshots a value at function entry, you can express relationships between the before and after:

```vary
class Account {
    mut balance: Int = 0

    def deposit(self, amount: Int) -> None {
        in { amount > 0 }
        post { self.balance == old(self.balance) + amount }
        self.balance = self.balance + amount
    }
}
```

That `post` block says: after `deposit` runs, the balance must equal whatever it was before plus the amount deposited. If someone later refactors `deposit` and introduces a rounding error or an off-by-one, the contract fires on the first call.

## Why bother

### Contracts outlive the person who wrote them

A test verifies specific examples. A contract verifies a rule that holds for every call, forever. When new team members add features, they do not need to know which examples the original author thought were important. The contract tells them what the function promises.

### Contracts document behaviour that comments cannot enforce

```vary
# b must not be zero   <-- a human might ignore this
def divide(a: Int, b: Int) -> Int {
    return a // b
}
```

versus:

```vary
def divide(a: Int, b: Int) -> Int {
    in { b != 0 }       # <-- the machine enforces this
    return a // b
}
```

The comment and the contract say the same thing. The difference: the comment is a suggestion. The contract is a wall.

### Contracts kill mutants for free

This is the part specific to Vary. The compiler has [mutation testing](/docs/mutation/testing/) built in, where it makes small changes to your code and checks whether tests catch them. Contract violations count as kills. If a mutant changes `self.balance + amount` to `self.balance - amount`, the `post {}` contract fires and the mutant is dead. No test needed.

In practice, functions with good contracts tend to have high mutation scores without many tests. The contracts already catch deviations from the specified behaviour, so the mutation engine has less work to do.

## Invariants: rules that always hold

Classes and data types can declare invariants that are checked after construction:

```vary
data PositivePoint {
    invariant {
        self.x > 0
        self.y > 0
    }
    x: Int
    y: Int
}
```

Try to create `PositivePoint(-1, 5)` and you get a `ContractViolation`. The type system guarantees the struct exists. The invariant guarantees it makes sense.

## Pure functions: no side effects allowed

`pure def` is related to contracts in spirit: it is a promise that a function has no side effects. The compiler enforces this statically (not at runtime). A pure function cannot call `print`, read files, or modify global state:

```vary
pure def add(a: Int, b: Int) -> Int {
    return a + b
}
```

If you try to call an impure function from inside a `pure def`, the compiler rejects it. This matters for mutation testing: pure functions are deterministic, so every mutant produces a stable, reproducible result. No flaky failures from timing or randomness.

## Combining all three

A function can use `in`, `post`, and `out` together. They run in order: precondition first, then the body, then state postcondition, then return postcondition.

```vary-snippet
def withdraw(self, amount: Int) -> Int {
    in {
        amount > 0
        amount <= self.balance
    }
    post { self.balance >= 0 }
    out(r) { r == amount }
    let prev = self.balance
    self.balance = self.balance - amount
    return amount
}
```

That is four promises in six lines: the amount is positive, the account has enough, the balance stays non-negative, and the returned value equals what was requested. If any future change to `withdraw` breaks any of these, the contract fires on the first call that hits the violation.

## When to use contracts versus tests

Contracts do not replace tests.

Use contracts when you can state a rule that should hold for every possible call: "the denominator is never zero," "the output is always positive," "the balance changed by exactly the deposited amount."

Use tests when you need to check specific scenarios, integration behaviour, or outcomes that depend on multiple components working together.

The strongest code has both. Contracts catch the structural guarantees, tests check specific scenarios, and mutation testing tells you whether the combination actually covers what you think it does.