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.