Interactive theorem provers like HOL and Isabelle use the static type checking in ML, where type safety is guaranteed, to guarantee soundness. Specifically, something of type "thm" (for theorem) must be true, because (I think this is how it works) only the axioms and inferences rules produces things of that type. At the same time, these systems are very extensible and you can write more powerful inference rules or functions that return theorems in ML... the type system ensures that the only way these functions can work is by proving their results, i.e. calling the low level axioms and rules.
Now I've been thinking about whether one could write something like HOL in Scheme. At the moment I'm thinking you could put the kernel (the axioms and inference rules) in a library along with a new theorem record type, and then not export any method for creating theorem records that isn't an axiom or rule. Would that guarantee soundness in the same way, or can you never really restrict how records of a type are created? Also, is it possible to do it without records or libraries (e.g. in R5RS)? Finally, let me know if there already exist theorem provers written in Scheme.
