主要观点：CakeML 是一种函数式编程语言及围绕其构建的证明和工具生态系统，包含多个组件且均为免费软件。
关键信息：

• 语言定义：基于 Standard ML 的子集，形式语义在高阶逻辑中，核心稳定，标准库仍在开发。
• 编译器后端：有多个部分，重要的已证能生成与源程序行为兼容的机器码，通过中间语言并优化。
• 编译器前端 1：能从 HOL 中的函数生成 CakeML AST 并证明行为相同，近期版本可处理 I/O 和状态。
• 编译器前端 2：由传统解析器和类型推断器组成，已证在声明规范下是可靠和完备的。
• 编译器自举：在 HOL 内部自举，通过前端 2 与后端结合实现。
• 程序后验验证：将 Charguéraud 的 CFML 验证框架应用于 CakeML。
• 验证应用：有多个端到端验证应用，如编译器、工具等。
• 验证编译器：用于构建其他编程语言的验证编译器。
  重要细节：
• 新闻方面：2024 年 3 月有 4 篇相关论文被接受，2024 年 1 月 POPL 2014 论文获 Most Influential POPL Paper Award，2023 年 6 月有 3 篇论文发表。
• 人员方面：有目前最活跃的开发者和众多贡献者，包括他们的相关信息，且得到 Zulip 赞助等。