Ruby 居然有人做形式化验证了？0条评论说说明了一切

Ruby 以动态类型和"开发者快乐"为信条，你很难把它和"类型健全性证明"画等号。可偏偏有人用 Lean 为 Ruby 搭出了完整的形式化语义，还给出了类型不崩的保证。1个点赞、0条评论——这消息在 HN 上像一片落叶，连风都没惊动。但这恰恰是问题所在：一门靠 Rails 撑起生态的语言，其核心语义居然没人系统性地验证过？作者做的不是给 Ruby 加速或提效，而是用形式化方法回答一个根本问题——Ruby 的行为到底能不能被严格定义？答案当然是能，但代价高昂、受众极窄。形式化验证从来不是为 Ruby 设计的，可正因如此，有人硬是做到了，才让这件事从技术练习变成了一场关于语言本质的实验。

原文：Ruby-lean: A Ruby semantics with a type soundness proof · 来源：Hacker News