The Coq mailing list

[Mario Carneiro <di.gama AT gmail.com>]

Does the Coq Coq Correct! project address the issues pertinent to this unsoundness bug? Last I checked they axiomatized the part that would have interacted with this guardedness condition: https://metacoq.github.io/metacoq/html/MetaCoq.PCUIC.PCUICTyping.html#ind_guard . This (and other "advanced" inductive extensions) is the part I find most dubious about Coq generally, so I really hope they get around to it at some point.

On Tue, Dec 28, 2021 at 10:00 PM Jason Gross <jasongross9 AT gmail.com> wrote:

> Would a hypothetical proof of consistency of the entire Coq kernel as it currently exists be possible in principle

You may be interested in the Coq Coq Correct! project, which re-implements a significant fraction of Coq's kernel in Gallina (I think everything except the .vo format, module types / functors, universe polymorphism, and the VM and native reduction machines, but don't quote me on this) and proves it correct relative to an axiom stating strong normalization of CIC.

Best,

Jason

On Tue, Dec 28, 2021 at 6:44 PM Abhishek Anand <aa755 AT pm.me> wrote:

I have a small side question regarding the wiki article. It contains a sentence:

> As a result, not all the legitimate functions that satisfy the current (unsound) guardedness checker will satisfy the new sized type based typechecker.

My impression was that all the actual soundness holes in the guardedness checker were patched, so what unsoundness remains in the checker in recent versions of Coq? Would a hypothetical proof of consistency of the entire Coq kernel as it currently exists be possible in principle, or do we know that this is false without avoiding certain areas?

Yes, as far as I know, the guardedness checker was patched. I fixed the article: https://github.com/coq/coq/wiki/CoqTerminationDiscussion/_compare/8f9576e00875b77614eae47dbd5cbbbc86c7adfd...fd05a250486919dc8035174017acf65667f66967

Mario Carneiro

On Tue, Dec 28, 2021 at 3:34 PM public <aa755 AT pm.me> wrote:

I wrote a wiki article about the last such incident I remember.

https://github.com/coq/coq/wiki/CoqTerminationDiscussion

(others have since contributed to the article)

Regards,

Abhishek Anand

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Tuesday, December 28th, 2021 at 3:19 PM, Marco Servetto <marco.servetto AT gmail.com> wrote:

> Hi,

>

> I'm writing a little document talking about soundness/unsoundesses in

>

> verification systems.

>

> I remember that there was a time we managed to prove False in Coq, and

>

> the community came together effectively and promptly to fix it, and

>

> all major proofs were unaffected by the fix. I also remember members

>

> from other communities (Agda?) coming to give a hand.

>

> While I'm not a Coq genius, seeing the honesty and the clear polite

>

> and direct action made by this community filled me up with hope for

>

> the

>

> future.

>

> Do I remember correctly? Can someone help me to summarise the event

>

> and provide some references? Do you have references to other important

>

> tools that have been proved unsound and any discussions about the

>

> response of their community?

>

> Marco.