法国用 MLang 编译器重写税法，实现可验证的计税代码

fkasummer · x · 2026-10-24

推文配图为 Inria、索邦大学与 Microsoft Research 合作的论文《A Modern Compiler for the French Tax Code》（arXiv 2021）。法国所得税由 DGFiP 用 1990 年设计的自定义遗留语言与编译器计算，代码老化、难以维护。团队通过逆向工程将其形式化，构建开源编译器工具链 MLang：具有形式化语义、消除手工工作流、可编译到 Python 等现代语言，并已通过 DGFiP 私有测试集验证。DGFiP 现已正式将生产系统迁移至 MLang，使税法计算可被独立复现、审计与模拟税改影响。引用推文感叹这类法律代码「迫切需要形式化验证」，这正是该论文的示范意义。