Hacker News Reader

Comment by yodsanklai | Hacker News Reader

I've always thought that Coq type checker was small enough to be formally verified.

What must be trusted in Coq in the kernel, which contains 30,000 lines of code for the latest development version.

It cannot be completely verified by Coq itself due to the Gödel theorem (well, now with this bug this is possible). Still, some part of it can be verified, like the byte-code interpreter. There is actually an ongoing project to make a certified JIT compiler for Coq: http://www.maximedenes.fr/download/coqonut.pdf

> It cannot be completely verified by Coq itself due to the Gödel theorem

What can't be proved in Coq is that the proof system is consistent.

However, we can in theory verify that the implementation of the proof system satisfies its specification (edit: maybe that's what you were saying!).

Doesn't the Gödel theorem say that such proof cannot be found for all conceivable systems; but that for any particular system, a proof could in principle be found?

It's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.

Is it possible to prove most of the system so that the remaining unprovable parts are minimized?

Yep.

And there are proof systems that use this approach (i.e. build a series of provers that each prove the next (more complex) one).

Unfortunately, it is sometimes the case that the remaining unprovable part is the most epistemologically dubious part.

See, for instance, "Coq in Coq", by Bruno Barras and Benjamin Werner, http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf , in which the Calculus of Inductive Constructions is used to prove the consistency of the Calculus of Constructions.

See also John Harrison's "Towards self-verification of HOL Light", http://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf , and Gentzen's consistency proof, https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof , which use similar strategies (by assuming the existence of an inaccessible and assuming recursion up to epsilon_0).

Sometimes one can get relative consistency results. For instance, I believe it is provable in ZF that if ZF is consistent, so if ZF+AC+(V=L)+GCH.

I think it's something like this: you can't prove the consistency of a formal system using that same formal system, unless it is in fact inconsistent, but you can model a formal system from inside a larger formal system and then prove things like consistency about the smaller system from inside the larger one. But then the consistency of the larger system is unproven and you're stuck with an endless regress into ever larger FS's as you pursue the chimera.

Only for sufficiently powerful systems, I believe.

Things like first order logic are too simple to introduce the kinds of statements Godel used to prove the incompleteness theorem about arithmetic.

Weirdly enough, as Gentzen showed, you can use a theory that is "sideways" to first-order logic, neither strictly more powerful nor weaker nor equivalent in power, to demonstrate the consistency of first-order logic. Strong normalization theorems are used for typed lambda calculi like the Calculus of Inductive Constructions to show consistency, as well.

It's not small at all. It's about 30KLOC of code.

Reply on news.ycombinator.com