你的类型检查器可能错了

Type checker may be wrong – Lean and the Curry-Howard correspondence

类型检查器通常被视为代码安全的守护者，防止我们在字符串和整数间犯错。然而，在 Lean 等证明助手中，类型检查器承担着验证数学定理的重任，其背后是 Curry-Howard 对应原理。文章深入探讨了如何将逻辑命题映射为类型，证明映射为程序。通过一个具体的 Lean 定理证明示例，展示了类型检查器如何验证逻辑推导。但关键在于，类型检查器在验证过程中必须确保所有表达式都能完成求值。如果程序陷入无限循环或无法终止，类型检查器就无法给出确定的结论。这意味着，在某些极端情况下，你依赖的类型检查器可能无法确认你的代码是正确的，甚至可能因为无法完成计算而显得“错了”。