Numbers are sets

Write three at the type level and the classic answer is a small tower: successor of successor of successor of zero. The shape is mathematically clean. For the questions a compiler asks about machine integers, though, walking a unary spine feels like bringing a family tree to a bounds check.

A numeric type can instead denote every value a term may still hold. I8 starts life as everything from -128 through 127, and the program itself whittles it down — a guard cuts values away, arithmetic shifts what survives. By the time you are three branches deep, the type is a running approximation of the number actually in your program.

Successor earns its place#

Lean introduces natural numbers with the familiar inductive definition: zero is a natural, and the successor of a natural is another natural. Three is therefore a nested proof object.

inductive Nat where  | zero : Nat  | succ : Nat → Natdef three : Nat :=  .succ (.succ (.succ .zero))

This representation is excellent when a proof follows the structure of Nat. Handle zero, assume the result for n, and prove it for succ n. Recursive definitions line up with the same eliminator. The official Lean chapter also introduces subtype notation such as {x : α // p x}, whose inhabitants are the values of a base type satisfying a predicate.

Machine-integer guards ask a different question: which inhabitants survive this branch? Your program compares offsets and lengths all day and inducts over unary numerals roughly never, so the checker needs a vocabulary for shrinking what an ordinary integer might be.

A branch cuts the set#

Consider a signed byte that must survive two positive checks. The source is ordinary control flow; the interesting part is what the checker can know at each line.

fn usable(n: I8) -> I8 {  if n > 0 {    let m = n - 3    if m > 0 { return m }  }  return 0}

The first guard is a straight cut. Subtraction is stranger — it does not shrink the set so much as drag the whole thing three places down. And if the checker keeps the equation m = n - 3 around, the later fact m > 0 travels backwards and sharpens n too, which is the little move that sold me on the whole framing.

F* makes the set interpretation explicit with let nat = x:int{x >= 0}. The LiquidHaskell tutorial gives refinements the same reading: a base type plus a logical predicate constraining its inhabitants. Neither checker needs to turn four into four applications of succ before proving that four is positive.

Intervals eventually lie#

One lower bound and one upper bound can only describe a solid interval. After n != 0, the exact set is [-128, -1] ∪ [1, 127], so an interval-only checker gets two options — forget the hole, or start juggling unions of ranges — and neither is free.

Relationships between variables cost more. Separate ranges for x and y cannot remember x < y once both ranges widen. Antoine Miné's octagon domain keeps constraints shaped like±x ±y ≤ c, enough to retain many differences and sums without paying for arbitrary polyhedra. Its matrix representation makes a specific trade between precision and analysis cost.

Fixed-width arithmetic adds another cut. A range crossing the wrap boundary can become two disjoint ranges, while multiplication introduces relations that no interval can express exactly. Abstract interpretation gives this engineering choice a name: the analyzer chooses an abstract domain, performs operations there, and accepts safe approximation when exact sets would explode. Cousot and Cousot's original formulation treats program execution through abstract objects instead of enumerating every concrete state.

I do not know a convincing way to make arbitrary nonlinear refinements feel predictable in ordinary editor feedback. A deliberately limited linear-integer arithmetic fragment still handles useful equalities and inequalities, while leaving a programmer some chance of understanding why a branch failed to prove its bound.

Keep both number systems#

Use inductive naturals where the proof genuinely follows zero and successor. For indexes, lengths, offsets, counters, and fixed-width values, let the type checker track a set or a deliberate approximation of one. A language can expose each view at the boundary where it fits.

F*'s factorial lecture reduces the safe recursive call to one obligation: n >= 0, n <> 0 ⊢ n - 1 >= 0. The branch removes zero, subtraction shifts the remaining set, and the recursive argument stays inside nat.

The last expression on that proof line is n - 1 >= 0. That is the fact the recursive call needs, and it fits without printing another successor.