Appendix C: Glossary and Learning Checklist
Make sure you can use what you have read.
C.1 A short glossary
| Term | Meaning |
|---|---|
| Proposition | A claim you want to prove true |
| Proof term | A value of the type corresponding to a proposition |
| Kernel | The small core that checks a proof term against its type |
| Dependent type | A type whose specific form depends on values |
| Structural induction | Proving the general case by following data constructors |
| Type class | A collection of operations and, where applicable, laws for a type |
| Ownership | Rules governing use, duplication, and disposal of values |
| Borrow | Temporary access without transferring ownership |
| Algebraic effects | Separating requested operations from their handlers |
| Continuation | The rest of a computation after a suspension point |
| Multi-shot | Resuming the same continuation more than once |
| Effect row | The set of effects a function leaves for its caller |
| Totality | Producing a result for every input in the domain |
| Trust boundary | Components trusted externally rather than established by the formal proof alone |
C.2 Check your understanding
After finishing the book, try answering these questions aloud:
- How do
letandvardiffer with respect to ownership and mutability? - Does Tauto apply a type as
Option(i64)orOption<i64>? - How do
affineandlineardiffer in the number of permitted resource uses? - What are the respective roles of
performandhandle? - Why does
resume ωinteract with static ownership checking? - Why can
Reflprove(2: Nat) + 2 = 4? - How does induction differ from a finite set of test cases?
- Can you distinguish what the kernel proves from what is trusted in a native runtime?
If you can explain these points, you have learned Tauto's basic syntax and the first ideas of proof-oriented software development. Next, give one small function of your own an invariant, then trace how its proof corresponds to individual lines of code.