Robin Milner, at the University of Edinburgh, develops from 1973 onward the ML (Meta Language) language as an auxiliary tool for his LCF system (Logic for Computable Functions), designed to verify computer-assisted mathematical proofs. ML introduces a complete, mathematically well-founded type-inference system — formalized together with Roger Hindley in what is known as the Hindley-Milner algorithm — that lets the compiler automatically deduce the data type of every expression in the program without the programmer having to declare it explicitly, while at the same time guaranteeing that the program is free of certain type errors even before it is run. ML also establishes, together with Lisp, the functional programming paradigm as a rigorous alternative to the dominant imperative programming, treating functions as first-class values that can be passed as arguments or returned as the result of other functions. The lineage of languages descending directly from ML — Standard ML, OCaml, F#, and, more indirectly, Haskell — becomes a reference field for programming-language research and a production tool in domains requiring high reliability, such as financial systems, compilers, and formal verification of critical software.