I was reading about HOL Light in its tutorial and I noticed that the distinction between theorem and term was made formal, but not in Coq. In other words, a theorem is a term that has been proved (and can only be the output of an inference rule or tactics), but that didn’t seem true in Coq (afaik).
Why? Why is this distinction not made Coq?
Related question: Terms vs Theorem vs Formula in Coq?
The presence of a thm type (at the metalanguage level) in HOL4 and HOL Light are consequences of design decisions taken by Milner when building the predecessor system (LCF). The so-called LCF approach is to reduce the soundness of the proof assistant to the soundness of the type system of the host/meta language (OCaml in HOL Light’s case): the implementation of the thm type is never exposed to users, who can only build terms of this type through documented operations whose soundness is known.
Coq doesn’t follow the LCF approach, and doesn’t much expose a metalanguage to users. The soundness of Coq is basically reduced to the soundness of (the implementation of) Coq’s standalone type checking algorithm, which is run, for example, when executing the Qed. command. The Coq designers had different goals and foundations in mind than Milner, and it doesn’t seem obvious why all proof assistants would or should have exactly the same design and implementation strategy.
I’m curious, what are some difference in the goals of Coq vs HOL Light? How did that translate to some of the design decision?
I’ll take this opportunity to compare some aspects of Coq and HOL, for future reference. There will inevitably be some overlap with answers in related threads.
Coq is based on dependent types and is inspired by Martin-Löf’s type theories from the 1970s. HOL builds on Church’s extensions to the lambda-calculus, in the form of simple types, from the 1930s. A basic distinction between Coq’s and HOL’s foundations is that the former allows types to be directly parameterized on terms, while the latter does not. The paradigmatic example is a type representing a vector space over real numbers, which in Coq may directly depend on a natural number for the dimension; in HOL the encoding must be less direct.
The propositions-as-types principle was important to Coq’s designers, and means that proofs (most directly, terms of types that live in Prop) are in principle built and processed in the same way as other terms, such as terms representing programs. In contrast, HOL proofs are essentially lists of Gentzen-style sequents and are exposed only indirectly at the metalanguage level, i.e., not as transparent objects in their own right.
Coq proofs (proof objects) are usually built and stored in full and are reasonably tractable to view thanks to support for purely computational reasoning steps. In contrast, HOL proofs are typically huge, do not contain implicit computation, and are almost never built in full or inspected by users.
Coq’s logic is constructive (intuitionistic) and its functions are computable by default. HOL’s classical logic conflates booleans and propositions and permits functions that aren’t computable or even fully specified. The SSReflect proof language and MathComp library for Coq can be viewed as reinstating boolean-based reasoning of the kind done by HOL users for dependent type theory.
Classical choice (of inhabitants in types) is included in HOL in the form of Hilbert’s epsilon operator, and key to this is that all HOL types are inhabited. In contrast, non-inhabited types such as False are central to Coq, and there is no classical choice without adding axioms.
HOL has a relatively straightforward interpretation (semantics) in terms of ZFC set theory, while Coq’s metatheory is much more involved, as can be seen in this thread.
For references on the implementation architecture of Coq, see this post and other replies in that thread.
A small addition:
Coq is more suitable for abstract algebra and category theory, as can e.g. quantify over all (small) groups.
This is impossible in HOLlight. Isabelle has “locales”, but they are not first class. I.e. one cannot quantify over them.