Programs with proofs
Put induction to work on programs. Write specifications that rule out wrong implementations, split proofs on a program’s branches, verify a reference implementation of list reverse and build on the lemmas you prove, show that an invariant survives every sequence of operations, and finish with a verified polymorphic iterator.
Progress is kept in this browser until you sign in
- Specify a functionThree properties that pin down a maximum, and split for the proof.12 min
- Safe division with OptionSpecify a partial function that returns none instead of failing.11 min
- Case analysis on inputsProve a fact about a pattern-matching function with cases.12 min
- Structures and round tripsSwapping a point twice returns the original point.11 min
- Verify your own reverseReversing a concatenation reverses the order of the pieces, by induction.15 min
- Build on a proved lemmaReversing twice gives back the list, with the previous law doing the hard step.13 min
- A Boolean search over a listSearching two joined lists is searching each part and combining with ||.13 min
- An invariant over every runA capped counter stays within its cap after any sequence of operations.16 min
- Project: verified iterationWrite a polymorphic iterator, prove its composition law, and verify a numeric specialization.24 min