OTOH, Coq is based on the Calculus of Inductive Constructions, which is both (a) more complex that the calculus of constructions, and (b) has an implementation in Coq that changes rapidly and is not formalized in any published paper, as I understand it.
Finally, do you know if this was a bug in the kernel, or if some other component (the compiler or caml virtual machine) can be blamed? It apparently was a problem with `vm_compute`, which I don't think I've ever used.
>The Calculus of Constructions is dependently typed, and it has a reasonably sized kernel, compared to HOL and ZFC:
However, Calculus of Constructions doesn't have inductive constructions, without which it's very hard to formalize interesting mathematics in it.
>Finally, do you know if this was a bug in the kernel, or if some other component (the compiler or caml virtual machine) can be blamed? It apparently was a problem with `vm_compute`, which I don't think I've ever used.
Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.
> Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.
> However, Calculus of Constructions doesn't have inductive constructions, without which it's very hard to formalize interesting mathematics in it.
Inductive types is something I've wondered about for a couple of weeks.
I know it's possible to simulate inductive types in some formalisms, then add them as a conservative extension. I think this is how HOL-Light works - inductive types aren't in the logical kernel, but they can be added without any new axioms.
To what extent is this possible in the Calculus of Constructions without inductive types?
Wiedijk has pointed out that it's impossible to prove "0 =/= 1" in plain CoC. Is this related?
Actually, AFAIU, you can define simple inductive types via church literals. However, you can't define induction principle for them. However, without induction principles, you can't prove anything useful.
For example, let's see how to define induction principle for Nat.
We should define two terms with the following types:
NatRec : (R : Set) -> R -> (R -> R) -> Nat -> R
NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)
For the first we can represent zero and suc as functions of the first type (it will be church literals). However, we can't do the same for the second. We can create a term which has that type but it won't typecheck.
Although this proof, it can be found in [1], is subject to the constraints that Goedel's 2nd theorem enforces: the proof uses a stronger logic that HOL itself. In this case it uses a large cardinal axiom.
As far as I know, the only system which achieves this goal is HOL.