> The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that yo

> The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified. That's what I mean. The LCF approach is to give you a signature with an abstract type thm and operations to construct its inhabitants. The operations are such that you can only construct valid theorems. Example (taken from http://www.cl.cam.ac.uk/~jrh13/slides/sri-20feb05/deduction.pdf http://www.cl.cam.ac.uk/~jrh13/slides/sri-20feb05/deduction....): module type Proofsystem = sig type thm val axiom_addimp : formula -> formula -> thm val axiom_distribimp : formula -> formula -> formula -> thm val axiom_doubleneg : formula -> thm val axiom_allimp : string -> formula -> formula -> thm val axiom_impall : string -> formula -> thm val axiom_existseq : string -> term -> thm val axiom_eqrefl : term -> thm val axiom_funcong : string -> term list -> term list -> thm val axiom_predcong : string -> term list -> term list -> thm val axiom_iffimp1 : formula -> formula -> thm val axiom_iffimp2 : formula -> formula -> thm val axiom_impiff : formula -> formula -> thm val axiom_true : thm val axiom_not : formula -> thm val axiom_or : formula -> formula -> thm val axiom_and : formula -> formula -> thm val axiom_exists : string -> formula -> thm val modusponens : thm -> thm -> thm val gen : string -> thm -> thm val concl : thm -> formula end;; With this type signature, the ML type system guarantees that only valid theorems can be constructed. Note that this is not Curry-Howard. Of course, you can punch holes into this by allowing unproved assumptions using mk_thm or the like. But the original idea was to implement all other tactics only using such a correct-by-design structure.