To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation.

Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).