This seems to be missing from the faq. I have a fairly good idea of the answer, but was surprised not to find this documented (in one place). Am I overlooking something?

I’ll let others actually answer the questions, but FTR the Coq FAQ has this page https://github.com/coq/coq/wiki/The-Logic-of-Coq which could be usefully completed with these questions, and their answers (anyone is welcome to edit it). [We also have plans to refactor the manual in a way that will g…

The closest answer in the FAQ is probably this one: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq I agree that this should also be in the manual. Also, one specific point I haven’t seen discussed “philosophically” anywhere is the reasonablen…

I’m provide references later, but there is a proof that a part of Coq is SN. There is the set theoretical model of pCuIC and the HoTT model. All cover large parts of Coq, but not all, as far as I know.

I feels like this section, from the FAQ question that you just linked to , is in serious need of being rewritten: I think the argument regarding the features that are used should be removed entirely. Furthermore, something should be added about the reinforced need to trust the OCaml compiler when u…

Strong normalization implies consistency. I believe this argument is due to Thierry, e.g. p15 here. ftp://ftp.cis.upenn.edu/pub/papers/gallier/sntoc.pdf However, the last time this came up. https://sympa.inria.fr/sympa/arc/coq-club/2016-02/msg00246.html It was not clear whether Coq is SN. Ther…

Coq is still not strongly normalizing (this is folklore among Coq developers): Fixpoint f (n : nat) := let a := f n in 0. Eval cbn in f 0. Fail Eval cbv in f 0. (* The command has indeed failed with message: Stack overflow. *) However, this is IIUC not endangering the consistency of Coq, even if i…

I think that warrants a bug report. The paper on the set-theoretical model conjectures that pCuIC is SN. @mattam ?

@Zimmi48 has this been documented? It sounds like something that should be fixed if we want the implementation of Coq to follow pCuIC.

You meant to ping @mattam82 in your previous message. BTW, he shared this paper yesterday, where it is again assumed that pCuIC is strongly normalizing. I don’t know if this is documented anywhere, and I didn’t find any issue about it. Feel free to create one.

Why is Coq consistent? What is the intended semantics?

Miscellaneous

palmskog July 8, 2019, 4:09am 5

I think it’s worth pointing out that while the kernel discussion in this post is in some sense distinct from the topic here, it also overlaps quite a lot.

Topic		Replies	Views
Does proof of coq consistency need axiom of choice? Miscellaneous	3	1125	February 6, 2020
Understanding the Coq kernel Using Rocq	5	4347	May 24, 2019
How can Coq accept an unsound proof if the kernel is correct? (failure modes, examples, and mitigations) Using Rocq	13	230	October 8, 2025
Notes from the CoqPL 2024 Q/A session Miscellaneous meeting	9	641	January 29, 2024
Experiment: Coq Code Interpreter in ChatGPT Announcements	3	571	January 12, 2024

Why is Coq consistent? What is the intended semantics?

Related topics