LeanReact 0.1 发布：用 Lean 类型系统表达组合正确的前端组件

hargup13 · x · 2026-09-18

作者发布 LeanReact 0.1，目标是在 Lean 定理证明器中表达可组合且正确性可验证的 React 组件。

核心思路：普通 React 写法的多个 useState 各自独立变化，一个多步结账组件的状态空间是 3×2×2×2×2 = 48 种组合，其中仅 10 种有效；真实组件状态远多于此，开发者几乎总会漏掉某些有效状态的边界处理。Lean 的类型系统能在类型层面排除不可能状态，把这类正确性保证从运行时提前到编译期。文中以多步结账为例展示了具体用法。