The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> That seems unlikely, since the CIC is not strongly normalizing:

The paper says:

In practice, our formalisation assumes strong normalisation of the reduction of CIC; and this even serves as the basis for the implementation of algorithmic conversion, which is defined by recursion on the strong normalisation assumption. We also assume other properties of the metatheory3: subject reduction, validity, strengthening, guard condition for inductive types and fixpoints and proof-irrelevance. This is the only Achilles heel of our formalisation, the correctness of the specification of the metatheory: If the metatheory fulfills the well-known, assumed properties, then there is no error in the implementation.

Maybe we can get one of the authors to comment?

Best,

Jason

On Wed, Dec 29, 2021 at 1:24 PM roux cody <cody.roux AT gmail.com> wrote:

On Tue, Dec 28, 2021 at 9:59 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.

That seems unlikely, since the CIC is not strongly normalizing:

Fixpoint foo (n : nat) :=
  let g := foo n in
  0.

Eval compute in foo 2. (* stack overflow *)

 

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.