20
$\begingroup$

By a bona fide bug in a proof assistant I mean a software flaw which is serious enough to create a possibility of "proving" something which is actually false. This is not a purely academic problem https://cstheory.stackexchange.com/questions/37299/has-a-proof-checker-bug-ever-invalidated-a-major-proof. We mathematicians do not have a real reason to care about it for now, but I am convinced that this problem has a good potential to grow to scary proportions once a large scale program of formalization of mathematics is attempted. Modern mathematics is more hierarchical then common software, and in a very nontrivial way. Because of this, a cleanup after fixing a bug may become rather painful.

I am curious about methods to avoid this which are based on mathematics (as opposed to some sort of management). One method I know about is verifying the code of a proof assistant using this same proof assistant. Strictly speaking, this is theoretically impossible due to the second Goedel theorem, but the way around it is to make the system stronger (for example, by adding a new axiom). There is a paper by J. Harrison about how it may be done for HOL light, J. Harrison, "Towards self-verification of HOL Light", Automated Reasoning, 2006 - Springer. More recent works in this direction are Myreen, Owens, Kumar, "Steps Towards Verified Implementations of HOL Light" , and Anand, Rahli, "Towards a Formally Verified Proof Assistant", ITP 2014: Interactive Theorem Proving.

Question 1. How far did it go? (All the above papers have the word ``towards'' in the title.)

Question 2. What can be said about formal verification of a proof assistant which may be of interest to mathematicians? (For example, are there nontrivial alternatives to, or variations of, self-verification?)

Remark. The question whether this or similar strategy actually makes a proof assistant perfectly bug-free (in the above sense) would be more appropriate on Computer Science SE, but I would not mind if anyone touches this topic.

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ Many would disagree with your view that '...mathematicians do not have a real reason to care about it for now...', including (respectfully) myself. $\endgroup$
    – James Smith
    Jan 24, 2018 at 12:36
  • 1
    $\begingroup$ @JamesSmith, with respect, your bio indicates that your work is in proof assistants, rather than in (research) mathematics. A counterexample to the OP's point would be an example of an active research mathematician who "care[s]". $\endgroup$
    – HJRW
    Jan 24, 2018 at 14:55
  • 4
    $\begingroup$ @HJRW : Voevodsky cared (though sadly he died not long ago). ias.edu/ideas/2014/voevodsky-origins He is survived by a thriving community of research mathematicians who actively formalize proofs of significant new theorems in homotopy theory. $\endgroup$
    – Timothy Chow
    Jan 25, 2018 at 3:37
  • $\begingroup$ @TimothyChow , Voevodsky is, indeed, one famous example. Are there proof assistants that can read proofs formalised in HTT? $\endgroup$
    – HJRW
    Jan 25, 2018 at 16:51
  • 2
    $\begingroup$ @HJRW : Sure, you can use Coq for example. Formally, homotopy type theory is not that different from conventional type theory, and Coq is sufficiently flexible, that it's not a big leap to use Coq for homotopy type theory. $\endgroup$
    – Timothy Chow
    Jan 25, 2018 at 20:09

1 Answer 1

Reset to default
10
$\begingroup$

See this dissertation by Ramana Kumar (Cambridge 2015). http://www.sigplan.org/Awards/Dissertation/2017_kumar.pdf

I present a proof of consistency of higher-order logic (HOL), in particular for the entire inference system implemented by the kernel of the HOL Light theorem prover [24]. The main lemma is a proof of soundness against a new specification of the semantics of HOL. This formalisation extends work by Harrison [23] towards self-verification of HOL Light. Using the proof-grounded compilation technique, I show how to produce a concrete implementation of a proof checker for HOL based on the verified inference system. The result is a theorem prover with very strong guarantees of correctness, and, as I will sketch, the rare potential to verify its own concrete implementation in machine code.

On a different note regarding HOL-varieties, there is also HOL Zero. http://proof-technologies.com/holzero/

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.