C*：让C语言编程与验证合二为一
C*: Unifying Programming and Verification in C
系统软件的安全至关重要，但传统验证工具往往将程序员拒之门外，导致开发和维护成本居高不下。C* 项目试图打破这一僵局，它通过扩展 C 语言，将验证能力直接融入编程环境。借助符号执行引擎和 LCF 风格的证明内核，程序员可以在编写代码的同时嵌入证明逻辑块，实现实时验证。这种设计让 C 语言成为实现代码与证明代码的统一载体，支持构建可复用的逻辑定义库和自动化证明工具。原型测试表明，C* 不仅能处理常见的 C 语言编程习惯，还能在 pKVM 的 buddy allocator 等复杂现实场景中有效应对推理挑战，真正实现了编程与验证的无缝融合。
编程与验证实践之间环境和范式的脱节，限制了验证的可访问性和实时性，成为阻碍程序员参与验证的关键障碍。
HN 评论区
41- eggy
我在这匹马上已经骑了很久了。最终我选择了学习 Ada/SPARK。Ada 2022 将开始为 SPARK 2014 提供新的更新。是的，它们都很啰嗦，如果你不喜欢这种风格，也不喜欢 Pascal 风格的语法的话。相信我，我喜欢 APL/J/k/uiua/BQN、Forth 和 ASM。只要编程语言及其生态系统（比大多数人认为的更重要）能满足你的需求，我通常对语法持中立态度。我在 2018 年尝试过 Rust，2023 年又试了一次，但发现它非常复杂，而且说实话，我不太喜欢它的语法。我本希望看到更多类似 ML 或 Haskell 的语法。Zig 看起来不错，但适用场景不同，而且太新了。毕竟，Ada/SPARK 在大型、高保障、高安全性的应用中已经运行了几十年。Rust 正在获得一些关注，反之亦然。AdaCore 曾开发过经过验证的 Rust 编译器，但随着现实世界产品（Blacktail hoist）的开发，我们需要一套工具集、保证、易于审计和验收的能力，以实现高安全性和标准认证。想想航空航天、国防、铁路和汽车行业。我从 1977 年开始编程，所以 ASM/C 在我心中始终占有一席之地。我玩过 F#、F* 和 MS 的 LOW，它们都不错，但它们和 Rust 都没有 Ada/SPARK 那样的现实世界积淀。我一直在使用 Shen 编写我们软件中非关键安全领域的形式化验证模型，我觉得这很令人耳目一新，不过，我的日常工作还是要专注于 Ada/SPARK，直到 Rust 在形式化验证方面更加成熟……
- gavinray
我真的认为，具备验证意识的语言将成为一种必需品。
最近写了一点关于这个的内容：
https://gavinray97.github.io/blog/design-by-contract-and-eff...
- IsTom
我和其他人一样喜欢分离逻辑的概念，但我觉得这个方案不行。看看那些例子，光是循环不变式就比整个示例代码还长。这不仅仅是易用性的问题，还留下了大量出现规范错误的空间。
而且我怀疑，既写 C 代码又需要形式化验证的人群，与形式化验证专家之间的交集并不大。
- Taikonerd
作者引用了这个，但顺便提一下：这听起来很像 F*，另一种面向证明的语言。（https://fstar-lang.org/）
F* 属于 ML 语言家族，所以它看起来和 C* 很不一样。
- slowcache
我觉得形式化验证是一个非常有趣的领域，但这对我来说行不通，因为我的键盘上没有倒过来的 E 键。