patternMajor
Do theorem provers demonstrate their own correctness?
Viewed 0 times
correctnessdemonstrateownproverstheoremtheir
Problem
I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong.
Basically, my question is: are automated theorem provers themselves ever formally proven to work with another theorem prover, or is there just an underlying assumption that any theorem prover was just implemented really really well, extensively tested & reviewed, etc. and so it "must work"?
If so, does there always remain some underlying doubt in any proof proven by a formally verified automated theorem prover, as the formal verification of that theorem prover still lies on assuming that the non-formally verified theorem prover was correct in its verification of the former theorem prover, even if it might technically be wrong - as it was not formally verified itself? (That is a mouthful of a question, apologies.)
I am thinking of this question in much the same vein as bootstrapping compilers.
Basically, my question is: are automated theorem provers themselves ever formally proven to work with another theorem prover, or is there just an underlying assumption that any theorem prover was just implemented really really well, extensively tested & reviewed, etc. and so it "must work"?
If so, does there always remain some underlying doubt in any proof proven by a formally verified automated theorem prover, as the formal verification of that theorem prover still lies on assuming that the non-formally verified theorem prover was correct in its verification of the former theorem prover, even if it might technically be wrong - as it was not formally verified itself? (That is a mouthful of a question, apologies.)
I am thinking of this question in much the same vein as bootstrapping compilers.
Solution
I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code.
There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant:
People put serious effort into these (well, at least the first four). For example,
steps 1 and 2 are addressed in Coq Coq Correct!, and steps 3 and 4 in the amazing award-winning CompCert project.
There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant:
- Verify that the algorithms used by the proof assistant are correct.
- Verify that the implementation of (the critical core of) the proof assistant is correct.
- Verify that the compiler for the language in which the proof assistant is implemented is correctly designed and implemented.
- Verify that the hardware on which the proof assistant runs is correctly designed and built.
- Compute the probability that a cosmic ray passes through the CPU and tricks your proof assistant every time you run it.
- Estimate the likelihood that you are insane.
People put serious effort into these (well, at least the first four). For example,
steps 1 and 2 are addressed in Coq Coq Correct!, and steps 3 and 4 in the amazing award-winning CompCert project.
Context
StackExchange Computer Science Q#119817, answer score: 46
Revisions (0)
No revisions yet.