News for hackers. Stuff that matters.

A comment on AI is forcing us to pay off 40 years of technical debt. Parent comment

Re:AI is forcing us to pay off 40 years of technical debt by c_engineer56 on Wednesday November 04, 2026 @04:42PM (#50371966)
How do you prove the correctness of your theorem prover?
[ Parent | on HN ]
Re:AI is forcing us to pay off 40 years of technical debt by drdeca on Thursday November 05, 2026 @12:20AM (#50375513)
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.

[ Parent | on HN ]