type theory and well-founded sets Program Verification Proving certain properties about programs—perhaps types, but not just types. Program verification proofs are usually written manually, but uses a proof assistant which… proof assistant Helps with proof, by: checking the proof for correctness (uses type theory) helps automate the easy parts