Indeed, a single syntax plays many roles in Coq: types and propositions, programs and proofs.

But be careful with words. â€śThey are the sameâ€ť is a vague statement: the same language can be used to say different things. Proving a proposition and implementing a program are still conceptually different activities (though the line between them can blur or even disappear at times). To make an analogy, we can give orders or recite poetry in English, but are orders and poems the same thing because theyâ€™re in the same language?

More technically, the words â€śtermâ€ť, â€śtheoremâ€ť, â€śformulaâ€ť donâ€™t have absolute meanings, and in fact even in Coq, they can reasonably be given quite different meanings. One should be precise about what they mean, especially when comparing concepts across languages.

In logic, a conventional definition might be as follows: a term is a bunch of symbols (most likely following some syntax), a formula is a term to which we can assign a truth value, and a theorem is a true formula. (There may be variations depending on technical details.)

In Coq, one could similarly say that a term is a bunch of symbols that follows the syntax of Gallina, a formula (or proposition, or type) is a term of type Prop (or sometimes Type), so a formula could be inhabited or not, and a theorem is an inhabited formula.

But in other theorem provers like, HOL Light, the distinction between a theorem and a term is rigorous. As I understand it, a term can only be of type theorem if it has actually been the output of a set of inference rules or tactics, but what I thought was weird is that Coq does not actually make this distinction explicit for some reason. Do you know why?

As was already answered in the question you linked to, HOL Light has a theorem type because it follows the LCF approach where you only build correct theorems by using safe primitives. The approach followed by Coq is that the kernel will type check any term you give it, and will reject any ill-typed term. Thus, you can have unsafe procedures generating proof terms, and soundness is ensured by the kernel being called to close a proof.