F*：让代码证明自身安全的编程语言

F*: A general-purpose proof-oriented programming language

▲ 182ducktective95 HN 评论区
F*：让代码证明自身安全的编程语言

F* 是一款面向证明的通用编程语言，由 Microsoft Research 和 Inria 等机构联合开发。它巧妙结合了依赖类型的表达力与基于 SMT 求解的自动化证明能力，支持纯函数式与效应式编程。F* 程序默认编译为 OCaml，也可通过 KaRaMeL 提取为 C、Wasm 或 F#，甚至利用 Vale 工具链生成汇编代码。从 Mozilla Firefox 到 Linux 内核，再到 Tezos 区块链和 Wireguard VPN，F* 已广泛应用于高保障密码学库 HACL* 和 EverCrypt 等关键基础设施中。无论是验证低层代码的安全性，还是构建形式化验证的解析器 EverParse，F* 都在推动软件正确性的边界。

F* 是一款通用目的的面向证明的编程语言，支持纯函数式编程和效应式编程。
阅读原文 →HN 评论区RSS

HN 评论区

95
  1. cyanregiment

    点了大概 5 页，愣是没找到一个代码示例。

    不知道为啥语言官网不把语法放在沙盒里，摆在首页最显眼的位置。

    这就像个游戏网站，连张截图或视频都没有（这种情况也遍地都是）。

    对于新编程语言，我只想要两样东西：

    1. 语法长啥样

    2. 我为什么要用这门语言

    聊聊证明逻辑，展示下语法，谢谢。

  2. LelouBil

    https://fstar-lang.org/tutorial/

  3. LelouBil

    我喜欢 Haskell，在我看来，这对想入门函数式编程的“新手”来说特别有用。

    这语言在业界有应用吗？用来开发什么类型的软件？

  4. pvsnp

    我喜欢能在逐步将现有的 C 代码库迁移到 F* 的同时，表达调用外部库的能力。这门语言非常扎实。

  5. boutell

    我想，响应式样式表如果不带副作用，大概是实现不了吧……

同日更多故事

2026-08-02