Etude VI

Dependent Types

Types that carry proofs of invariants and obligations.

Core Notes

Types carry proofs: Delta(s) is only inhabited when it is inflationary with respect to merge.

Delta(s) : { d : S | s ⊑ merge(s,d) }
The invariant lives in the type, not in comments. Rejection is a type error, not a runtime surprise.

Applied Thread

Applied to APIs: send value + proof witness, server checks proof and merges without revalidating state history.

trace: Def → Check(typing) → Counterexample(untrusted delta) → Repair(certify)