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.