Why is Coq consistent? What is the intended semantics?

[palmskog]

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.