从 LCF 到 OCaml：一门说"不"的语言

OCaml 源自 Robin Milner 为 LCF 证明器设计的元语言 ML，其类型系统保证被类型检查器接受的程序不会出错。OCaml 5 于 2022 年 12 月发布，带来跨核并行与代数效应，团队为此投入超过八年。Astrée 曾用它证明 Airbus A340 的 132,000 行 C 飞控软件不会因运行时错误而停止，Airbus 随后将其用于 A380。