C*：统一 C 语言编程和验证

【HN用户评论摘要】 我已经骑这匹马有一段时间了。我决定学习 Ada/SPARK。 Ada 2022 将开始提供新的 SPARK 2014 更新。是的，如果您不喜欢这类事情，也不喜欢类似 Pascal 的语法，那么它们都很冗长。相信我，我喜欢 APL/J/k/uiua/BQN 和 Forth 和 ASM。我通常对语法不可知，只要 PL 和生态系统（比大多数人想象的更重要）能够满足您的需求。我在 2018 年尝试过 Rust，然后在 2023 年再次尝试过，但发现它非常复杂，好吧，不喜欢 我真的认为验证感知语言将成为必需品最近写了一些关于此的内容 https://gavinray97.github.io/blog/design-by-contract-and-eff... 到目前为止，C 后继语言的名称已经耗尽，所以我表示同情，但我强烈地将 C* 这个名称与十年前关于 C 编译器积极利用未定义行为的咆哮联系起来：https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20...。 （我称其为咆哮并不是说它完全没有说服力。它的风格只是比我习惯在《计算机现代》中看到的排版更辛辣一点。） 作者引用了这一点，但只是提一下：这听起来像 F*，另一种面向证明的语言。 (https://fstar-lang.org/)F* 属于 ML 语言系列，因此它看起来与 C* 有很大不同。 已经有一个 C* ： https://en.wikipedia.org/wiki/C* 原始链接：https://arxiv.org/abs/2504.02246