a language that would only allow the writer to construct valid proofs with its polymorphic type system. ML was turned into a compiler to simplify using LCF on different machines, and, by the 1980s, was turned into a complete system of its own. ML would eventually serve as a basis for the creation of OCaml.

In the early 1980s, there were some developments that prompted INRIA's Formel team to become interested in the