| As a point of possible interest to people who are interested in programming language history, I'm going to elaborate a bit on this topic: The root of this particular family tree is essentially a fusion of the lambda calculus-inspired parts of Algol 60 and Lisp with some new ideas for syntax that were promoted by Peter Landin in his highly influential paper from 1966, "The Next 700 Programming Languages". He called this language ISWIM; it was studied extensively but never directly implemented. Landin was also associated with Dana Scott and Christopher Strachey in their foundational work on programming language semantics. Robin Milner was interested in the relationship between the logic underlying the semantics of programming languages and the possibility of using computers to prove propositions in that logic (a logic developed by Dana Scott in support of his semantics work). At Stanford, he and a small team (including Whitfield Diffie, who later went into cryptography...) developed a system called Stanford LCF (for Logic of Computable Functions). This was an interactive system in which the user states a main goal in the logic, then splits it to subgoals and more subgoals until they can be solved directly. Proofs were represented directly by data structures and were built directly by the proof manipulation commands, which corresponded to the inference rules of the system. Milner moved to Edinburgh in 1973, where he worked on a subsequent version of LCF, Edinburgh LCF. Stanford LCF was limited by the size of the proof data structures; for Edinburgh LCF Milner had the idea to forget the proofs, but store the results of them; i.e. the theorems. The proof steps would be performed, but not recorded. To ensure that theorems could only be constructed via valid proofs, a meta-language was developed with a static type system that would only allow data structures corresponding to valid theorems to be built. It also allowed more sophisticated proof development, since the meta-language was a full higher-order programming language modeled after Landin's ISWIM. Exceptions were included to deal with the possibility of failure of particular proof strategies. This version was implemented in Lisp. LCF spread to other universities; it was early on split into two parallel tracks, ML and Caml. Both have continued to be strongly associated with implementation of theorem proving systems. ML and LCF have become Standard ML and HOL; Caml has become OCaml and Coq. A lot of programming language research has also gone into ML and OCaml as languages in themselves due to their close association with the logic underlying semantics of programming languages. Meanwhile, a language called PAL was developed in 1968 at MIT in response to ISWIM and Strachey's ideas on programming languages. David Turner, while starting his Ph.D. research at Oxford, got access to the PAL sources and used a simplified form of the language as the basis for his lectures on functional programming at St. Andrews; he called this language SASL. It was initially just a blackboard language, but a colleague surprised him by implementing it in Lisp. In 1976, Turner changed the semantics of SASL from eager to lazy, based on a lazy version Landin's SECD machine. Somewhat later in his career, he combined ideas from lazy SASL, a cut-down version of SASL called KRC, and the ML-originated Hindley-Milner type system to form a language called Miranda. And Miranda is one of the primary influences on Haskell. So, this leaves out a lot of other languages such as HOPE and lazy-ML that also were developed in this space. But what's interesting to me is how all these languages, from ML to Haskell, are so strongly related to Algol and thus the Pascal, C, Java, etc. languages that are more familiar to industry. That got a lot bigger than I intended; I hope someone takes some interest from the digression. |