Theorem prover which extracts programs from proofs
