Caml was also initially implemented in LeLisp if I recall correctly. :-). An advantage of ML for theorem proving à la LCF is that you can use the type system t

Caml was also initially implemented in LeLisp if I recall correctly. :-). An advantage of ML for theorem proving à la LCF is that you can use the type system to enforce some invariants ; namely you can prevent the user from ever building a value of type `theorem` that is not actually a valid theorem. I don't know how that would work in a dynamic language where you have access to everything.