为交互证明设计的元语言
ML的名称来自“元语言”，最初是人们编写证明策略、与证明系统交互的工具。1973年起，罗宾·米尔纳及同事在爱丁堡大学发展可计算函数逻辑系统LCF，把处理证明过程的程序语言与被证明的逻辑表达式分开。早期团队包括马尔科姆·纽维、洛克伍德·莫里斯，迈克尔·戈登和克里斯托弗·沃兹沃思随后加入。
研究者面对的问题既是灵活性，也是可信性：用户需要组合不同证明步骤、编写可重复执行的策略，而一个策略程序即使出错，也不应轻易把任意命题冒充成定理。ML因此把函数、类型检查和受控制的数据构造结合起来，逐渐超出单一证明系统，成为通用语言发展的起点。
类型保护与失败处理
在LCF中，定理用抽象类型thm表示。用户通过代表合法推理规则的操作得到该类型的值，内部表示则隐藏起来。由这些操作组合出的证明策略可以很复杂，但策略不能直接制造一个未经推导的定理值。可信边界集中在实现逻辑推理规则的核心及其类型接口。
证明搜索常会走入死路，因此早期ML具有失败报告和捕获机制：某种策略失败后，程序可尝试另一种策略。它也允许函数像普通数据一样被传递，用较小策略组织较大策略。函数式核心之外，还存在可更新变量和循环，实际语言同时支持表达式计算与需要状态的操作。
一个函数处理不同类型的列表
米尔纳1978年的论文系统说明了参数多态和类型推断。以map为例，它把一个函数逐项用于列表。若f把整数加一，那么map作用于f和列表[1,2,3]会得到[2,3,4]；换成把整数转为真假判断的函数，输出则是布尔列表。遍历结构相同，元素与结果类型可以变化。
编译器从取表头、构造列表和函数调用之间的约束推导类型，不要求用户在每个位置重复填写声明。它会要求输入列表元素与f的参数类型一致，输出列表元素与f的结果类型一致。论文给出类型检查算法和可靠性论证，排除把整数当作函数等类型混用。
参考：[2]
从DEC-10走向VAX
早期LCF中的ML经翻译成为Lisp代码，在DEC-10环境中运行。卢卡·卡尔代利从1980年开始开发VAX上的实现，使用Pascal编写编译器和运行系统，并生成机器码。这条路线把ML从依附证明系统的实现方式，推进到可独立分发、供更广泛程序使用的工具。
1982年3月保存下来的《Edinburgh ML》分发说明明确针对VAX-VMS。用户从软盘复制文件后运行链接命令建立系统，再通过命令文件进入ML环境。说明还列出数组与lambda演算示例程序，并分别讨论ML堆、垃圾收集区和编译期间使用的Pascal堆。语言的传播已经具有具体安装包、运行入口和存储管理需求。
1983年的整合提案
不同实现积累的扩展也带来差异。米尔纳在1983年6月的第二版手稿中回顾，早期DEC-10版某些部分不完备、另一些部分冗余；卡尔代利的VAX版本修正了若干问题，而HOPE语言提供了另一些可借鉴的设计。1983年4月，他在伯纳德·苏夫林推动下提出整合ML的初步方案。
随后讨论汇集了罗德·伯斯托尔、卡尔代利、戴维·麦奎因、戈登等研究者的意见。标准化的目标是在保留语言基本性格的同时整理语法、类型、状态和程序组织方式。这些讨论推动ML从各自扩展的实现走向共同设计的标准语言。
参考：[4]
语言家族与形式定义
1990年出版的《Standard ML定义》为标准语言提供正式说明，1997年修订版由米尔纳、马兹·托夫特、罗伯特·哈珀和麦奎因共同署名。定义把核心语言与模块语言分开，并以静态语义说明类型与名字如何成立，以动态语义说明程序怎样执行。实现者因而有超出单一编译器行为的共同依据。
ML的历史遗产包括无需大量显式声明的静态类型推断、可复用的多态函数、抽象类型和模块化组织。Standard ML是这条发展线中的标准化分支，其他ML家族语言各有演变；早期证明工具、1980年代实现扩散与后来的正式定义，共同构成其从专用元语言走向通用编程的过程。
参考：[5]