Hacker News new | ask | show | jobs
by cmrx64 2707 days ago
not coq but HOL4 and Poly/ML. there are verified HOL kernels but you’d need to do substantial manual validation of the exported theorems to make sure they didn’t get subverted during proof export.