Hacker News
points by c_engineer56 3 days ago | 0 comments
How do you prove the correctness of your theorem prover?
[–] drdeca 3 days ago
Depends which way you mean. It is possible to provide a formal specification for a proof verification engine and prove, in the same language that the engine is for, that the engine implements that specification.

Proving that the system it implements is like, logically sound, is a different issue, and for that you do need stronger axioms.

Hacker News