Contract & Refinement Types
Behavioral guarantees checked before the code ever runs. Typestate systems,
refinement types, and design-by-contract annotations (Eiffel-style
pre/postconditions, Dafny requires/ensures) ask the compiler to prove
that certain behaviors are impossible, not merely unlikely.
Where a type checker answers “do the shapes fit?”, a
refinement type answers “can withdraw(amount) ever be called with
amount > balance?” — a behavioral claim, discharged at build time.
Sensor properties
| Property | Value |
|---|---|
| Oracle strength | High — a proof is the strongest oracle short of running the system |
| Independence | High — the checker cannot be gamed by the code it checks |
| Scope | Function to module |
| Feedback latency | Milliseconds |
| Actionability | Blocking — a failed contract stops the build |
| Type | Predictive |
What it cannot detect
Contracts only cover what was specified. The specification itself is written by the same mind that wrote the code, which is why contract checking composes with rather than replaces example-based tests and property testing.