微软系形式化验证语言F*编译多后端
推荐指数 56.0 NO. 013 · 2026.08.03
发布2026/08/02Score107Comments35
为什么值得看
F*是支持依赖类型和SMT自动证明的通用编程语言，可编译到OCaml、C、Wasm及汇编。对需要高可靠性保证的AI基础设施（如加密协议、分布式系统）有独特价值，能在开发阶段就消除整类运行时错误。
编辑判断
形式化验证圈子长期被Coq和Isabelle统治，但Coq的提取机制到高性能语言一直不够顺滑，Isabelle则更偏数学证明。F*的差异化在于原生支持effectful编程（状态、异常等副作用），这对实际系统代码更友好，而且KaRaMeL到C的提取路径在密码学领域已被Project Everest验证过生产级可用。
AI工程师可能觉得这东西离自己很远，但如果你在写任何不能出错的底层组件——比如模型推理服务的调度核心、联邦学习的加密聚合模块、或者GPU内存管理器——F*相比Rust的'尽量不出错'是'证明没错'，代价是写证明的时间。目前社区规模还很小，但微软研究院和Inria的持续投入意味着工具链在成熟，值得关注其是否会成为高可靠性AI系统的默认选型。
社区反馈
意见分歧 29 条评论
核心争论：F*语言能力受认可，但官网入门体验差、代码示例难找引发激烈吐槽
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?
Clicked like 5 pages and never found 1 code example. Idk why languages don't have their syntax in a sandbox front-and-center on the home page. It's like a video game site with zero screenshots or videos (also rampant). New programming languages I want 2 things: 1. What does the syntax look like 2. W