Type systems you can argue with

Refinement types have spent twenty years as a research curiosity. The tooling finally caught up, and the argument for them changed from elegance to economics.

Every type system draws a line between the properties it will check and the properties it will let you assert. Move the line and you trade compile time and cognitive load for a class of bugs that stops existing. The interesting development of the last few years is not that the line moved — it moves constantly — but that the cost of moving it fell far enough that the trade is now worth making in ordinary code, rather than only in avionics and cryptography.

The shape of a refinement#

A refinement type is a base type plus a predicate. Where an ordinary signature says a function takes an integer, a refined one says it takes an integer greater than zero, and the compiler discharges that obligation at every call site by handing it to a solver. The syntax is unremarkable; the consequence is not.

#[requires(idx < xs.len())]
fn get_unchecked<T>(xs: &[T], idx: usize) -> &T {
    // No bounds check is emitted: the caller proved this.
    unsafe { xs.get_unchecked(idx) }
}

fn sum_prefix(xs: &[i32], n: usize) -> i32 {
    let mut total = 0;
    let mut i = 0;
    // The loop invariant i < n <= xs.len() discharges the
    // precondition above on every iteration.
    while i < n && n <= xs.len() {
        total += get_unchecked(xs, i);
        i += 1;
    }
    total
}

The thing to notice is what did not happen. No proof was written. No tactic language was invoked. The obligation was generated by the compiler, shipped to an SMT solver, and discharged in single-digit milliseconds — and if it had failed, the error would have named the call site rather than the theorem.

The barrier to verification was never that engineers cannot reason about invariants. It was that the tools made them write the reasoning down twice.

Why now#

Three things converged. Solvers got substantially faster at the fragment that actually appears in systems code — linear arithmetic over bounded integers, with arrays. Compilers grew the intermediate representations needed to generate obligations without a separate front end. And, least discussed but probably most important, error reporting got good enough that a failed obligation reads like a type error instead of a proof-assistant transcript.

1. Solver throughput on the relevant fragment improved by roughly two orders of magnitude over the decade, mostly through better preprocessing rather than better core search.
2. Borrow checking normalised the idea that the compiler may reject a correct program because it cannot see why it is correct.
3. Incremental checking made the feedback loop interactive, which is the difference between a tool engineers use and a tool engineers schedule.

That third point deserves more weight than it usually gets. A verification tool with a ninety-second turnaround is a batch job, and batch jobs get run before releases. A verification tool with a two-second turnaround is a type checker, and type checkers get run on every keystroke. Nothing about the underlying mathematics changed between those two products.

A proof obligation that arrives while you are still holding the context in your head costs almost nothing. The same obligation delivered an hour later costs the whole context reload.

Where it still hurts#

Refinements are excellent at properties that are local and arithmetic, and poor at properties that are global and temporal. Anything phrased as "eventually" or "for every interleaving" remains firmly in model-checking territory, and pretending otherwise leads to the failure mode where a codebase accumulates enormous decorative predicates that prove very little at considerable cost.

The pragmatic position is to refine the boundaries — indices, capacities, lifetimes, units — and leave the interior alone. That captures most of the bug classes worth eliminating and almost none of the annotation burden that historically killed these systems.