What Is Guaranteed, and What Is Not
Read the trust boundaries between code, proofs, and the runtime.
20.1 State what is being checked
Formal verification requires careful reading of the exact claim a proof establishes. For example, sort_correct states sorting properties; it does not guarantee memory use, execution time, or external-library behavior.
| Subject | How it is treated |
|---|---|
| Whether a proof term has the proposition's type | Checked by the proof kernel |
| General properties expressed by induction | Checked according to the proposition and proof term |
| Runtime ownership and borrowing | Checked by separate static usage rules |
| Native runtimes and backends | Some implementation trust remains |
External functions called through extern | The correspondence between declaration and implementation must be trusted separately |
| Time and memory bounds for arbitrary execution | Require separate proofs or host-enforced limits |
20.2 Interpret a successful check
A successful tauto check does not establish that an entire program is completely safe. What matters is which assumptions each checked declaration uses, which pure functions it concerns, and what it proves about them. Axioms and extern declarations are part of this trust boundary too.
Use --json to inspect which axioms each declaration depends on.
tauto check examples/proofs.taut --json
Each declaration in the output includes its list of axioms. A declaration without axioms has an empty list. Chapter 14's not_not has ["em"].
20.3 Relate proof types to runtime types
In the proof layer, Nat represents arbitrarily large natural numbers in principle. Execution or extraction may represent them with fixed-width integers. For programs whose values exceed that range, consider possible differences between mathematical operations and runtime arithmetic.
Similarly, reference-counted shared values may not be released when reference cycles arise. Checking ownership is not the same as ruling out every resource leak.
20.4 Reduce the trust boundary
A practical workflow is:
- Design the pure core as small functions.
- Prove their invariants.
- Make runtime code call the same functions.
- Test and audit the boundaries.
This makes proofs more useful while keeping their uncovered areas visible.
Exercise 20.1: Why is a proof that sort is correct separate from the safety of reading its input from a file?