Salt v1.0.0 —— 一种在编译器中集成Z3定理证明的系统语言

- Salt 是一门新发布的系统编程语言（v1.0.0），其最大特点是**编译器内置了 Z3 定理证明器**，能在编译阶段自动验证代码的正确性（如数组越界、整数溢出、空指针解引用等）。 - Z3 是微软研究院开发的高性能 SMT（可满足性模理论）求解器，广泛应用于形式化验证、软件测试和人工智能等领域。Salt 将其直接集成到编译流程中，而非作为外部工具。 - 这意味着开发者可以用类似 C/Rust 的语法编写底层代码，同时获得接近形式化验证级别的安全保障，而无需单独编写证明或使用独立验证工具。 - Salt 的出现代表了“让形式化方法变得实用”这一趋势：把原本需要专家才能使用的定理证明能力，直接打包进普通开发者日常使用的编译器里。