What to Build Next

Combine what you have learned into a small verified program.

21.1 Suggested learning projects

You do not need to begin with a large theorem. Start with a small input space and explicit states and transitions; this makes the connection between programs and theorems easier to understand.

Project	First implementation	Next theorem
Counter	Increase and decrease a `Nat`	It never falls below zero
Permission flags	Switch between open and closed	A closed state does not decrement
List reversal	Recursive `reverse`	Reversing twice returns the original list
Maximum	Choose by comparison	The result is at least each input
Sorting	`insert` and `sort`	Sorted output with preserved elements

21.2 Break the problem into small parts

Develop in this order:

Specification: State clearly in plain language what success means.
Types and data: Describe possible states and inputs with enum and struct.
Pure computation: Write fn definitions while separating effects where possible.
Small examples: Use run and test to check intended behavior.
Propositions: Declare invariants with theorem, Eq, and related tools.
Proofs: Use constructor matching, lemmas, and equality rewrites.
Boundaries: List external operations and runtime-dependent components.

21.3 Take the next step

The repository's examples/ directory contains larger versions of topics introduced here:

sort/: insertion sort for arbitrary Ord types, with proofs.
bst/: a binary search tree representing a set, with proofs.
compiler/: compiling arithmetic expressions to a stack machine, with a correctness proof.
effect-proofs/: effect handlers calling proved transitions.
certified-state/: connecting proved state transitions to runtime code.

Once natural-number arithmetic is familiar, explore the relationship between Prop, inductive, and Type. If effects interest you, investigate how resume ω interacts with state and ownership.

Finally, prioritize small, precise assumptions and conclusions over impressive theorem names. That leads toward software whose meaning can be read and mechanically checked in Tauto.