Verified extraction from the Coq proof assistant to OCaml, synthetic computability, and machine-checked undecidability proofs.