智能体时代，Rust为何成为AI编程首选？

AI大模型正在重塑编程这件事，不少开发者开始焦虑：我的技能还有价值吗？编程语言设计还有意义吗？B站UP主分享的Nick Matzakis（Rust核心团队成员）的文章《What Agents Mean for Rust, or Vice Versa》，恰好回应了这些存在主义式的困惑。作者从五年级在5MHz的X86处理器上编程讲起，指出编程的本质多年未变，直到AI Agent的出现才带来真正的翻转——既令人兴奋，也令人恐惧和迷失。

智能体时代，Rust凭什么受青睐

Rust的流行度数据本身就很有说服力：在增长最快的语言中Rust位居第二，TypeScript同比增长率高达1200%；更惊人的是，Meta工程师今年编写的自有Rust代码量是过去9年总和的两倍。David Turner强调，部分原因在于Agent让尝试性事物变得容易，另一部分在于Rust以高性能著称——如果选择任何语言的难度都差不多，为什么不选执行速度更快的那个？

作者认为还有第三层原因：Rust恰好非常适合agentic coding。他提出高效软件工厂的三大支柱——设计、构造、优化。Rust在优化上天然占优：默认提供优异性能，同时保留多种可调优手段，比如精确控制数据在栈还是堆上分配、指针间接访问的位置、强制指定结构体内存布局，甚至嵌入内联汇编。过去性能调优带有神秘色彩，如今Agent让这一过程容易得多——从事超高性能密码算法开发的工程师表示，正从手工调整汇编转向借助Agent完成同样工作；构建网络服务时，配合Dial等性能分析工具，Agent能有效识别长轮询、阻塞等异步性能陷阱。

可靠性始终为王：类型系统是Agent的护栏

性能吸引人使用Rust，可靠性让人留下来。OpenAI的Greg Brockman曾表示，Rust在编译通过时基本能保证正确性，因此是构建Agent的理想语言。作者认同这一判断：像Rust、OCaml、Haskell这类语言有一种"编译通过就能正常运行"的感觉，Agent同样从中受益。

仅靠测试远远不够——测试可以证明缺陷存在，却无法证明缺陷不存在。作者常遇到前几个测试看起来很完美、下一个测试却完全失控的情况，深入排查后发现是Agent完全误解了自己试图表达的逻辑。这正是类型系统的真正优势：它提供护栏，确保Agent始终沿着正确轨道运行。在Rust中，护栏不仅限于字段名称是否正确这类技术检查，还延伸到"永远不要手动关闭Socket"等更高级的保障。

但类型系统也有固有局限：它只能保证你没有犯错，不能告诉你是否做了正确的事。要更进一步，就需要证明系统。Rust生态已有不少有趣的证明工具，可以证明代码不会panic，还可以添加断言验证代码确实计算出预期结果。

类型系统是编程语言中一组根据程序结构和用法对值、表达式和变量进行分类和约束的规则，最核心的作用是在编译期而非运行期发现并阻止不合法的操作。从只区分整数与浮点数的简单类型系统，到Haskell、OCaml、Rust所采用的带参数化多态、代数数据类型和所有权/借用检查的强类型系统，其约束力逐级增强。类型检查器会在代码真正执行之前遍历整个程序，构造类型推导并验证每一步操作都满足既定规则，因此凡是能通过编译的程序，都在被证明的范围内排除了整整一大类错误，例如把字符串当作数字相加、访问已释放的内存、违背接口契约等。这正是文中"编译通过就能正常运行"这种直觉的技术来源：类型系统本质上是一种自动化的、低成本的轻量级证明，它把许多运行期才暴露的缺陷提前到了编写阶段，也正因为这种确定性，它才成为约束AI Agent行为的天然护栏。

形式化证明：让Unsafe代码不再令人紧张

部署形式化证明不仅确保正确性，还能提升开发效率——这听起来反直觉，但事实如此。部分密码学算法具有非常清晰的数学结构，你可以基本告诉Agent：随意实现，只要能证明代码仍然计算出正确结果即可，这些证明可通过Lean或ARC等定理证明器完成。

一个典型场景是Unsafe代码：人们有时用它提升性能，但部署时保持紧张，因为一旦出错风险得不偿失。如果能借助形式化证明工具验证Unsafe代码实际安全，就可以毫无顾虑地进行各种优化。那有了证明系统是否还需要类型系统？作者的回答是绝对肯定——类型系统的使用要简单得多，因此更受欢迎；借助类型系统排除各种头疼的bug，才能把证明的精力集中在真正重要的部分。

形式化证明是用数学方法严格论证程序满足特定性质的技术，区别于测试的抽样验证，它要求对程序在所有可能输入和所有可能执行路径上的行为给出逻辑推导。常见做法是把程序语义转写成逻辑命题，再借助定理证明器（如Coq、Lean、Isabelle）或依赖精化类型、SMT求解器等工具完成机器可检验的证明。Rust生态中已有Kani、Creusot、Prusti、Verus等工具，可分别验证代码无panic、无未定义行为、满足函数前后置条件或计算出预期结果。其代价是编写证明与维护规格说明需要额外投入，且证明工具对语言特性的支持往往滞后。因此形式化证明在实践中通常只用于密码学、操作系统内核、安全关键系统等对正确性要求极高的模块，作为类型系统之外的第二道防线，而不是替代类型系统。

Rust中的unsafe关键字并不关闭借用检查器或类型检查器，而是解锁五项编译器无法自动验证的操作：解引用裸指针、调用unsafe函数、访问或修改可变静态变量、实现unsafe trait、访问union字段。这些操作之所以需要显式标注，是因为编译器无法证明它们安全，正确性责任被转移给程序员，并须由程序员自行保证满足Rust的别名与内存安全规则。一旦违反，程序可能产生未定义行为，其后果是编译器被授权进行任意优化，表现为难以复现的崩溃、数据损坏甚至安全漏洞。Unsafe代码的典型用途包括实现底层数据结构、与C语言交互的FFI边界、性能敏感的密码学原语等。业界通常通过将unsafe封装在小的、经过审查的安全API边界内来控制风险，这也正是文中强调库有责任保护用户免受未定义行为影响的原因。

北极星目标：不再出现Unsafe代码

作者为Rust提出一个北极星目标：不再出现Unsafe代码。他并非指永远不使用unsafe关键字，而是指具备能力证明所有编写的Unsafe代码都是正确的、不会引发未定义行为。明确知道哪些代码需要审查本身就是巨大进步；库有责任通过安全的API边界保护用户免受未定义行为影响。鉴于AI Agent在发现漏洞方面的能力，若要遏制持续不断的漏洞数量，就必须提升自身的技术水平。

设计方面仍是开放性问题。目前主流做法是基于Markdown的开发实践——编写文档并期望Agent关注。作者不确定Rust能在这些领域发挥多大作用，但认为可以采取一些步骤：提供把接口与实现分离的方法以便单独审查接口，或更清晰地查看Agent在接口上所做的更改，或提供更好的审查工具。他还认为存在专门用于设计的语言空间——一种能让你跟Agent快速迭代高层设计和不变量、而不需要深入代码细节的工具。

设计语言：最关键的突破所在

作者推荐了MacBlock的文章《现在容易的是什么，现在困难的又是什么》，其中指出任务的成功标准越能明确界定，任务就越容易完成。传统上被认为困难的任务将很快实现自动化，过去被视为简单的任务可能变得更有价值。从编程语言角度看，最关键的突破将来自设计语言——那些能在极高层面上捕捉架构和预期行为的工具，目标是让人类直观地指定设计，并自动转化为有效的验证机制，比如类型检查、代码规范检查或定理证明；随后Agent负责把设计转化为传统语言（如Rust）的编写代码，人类只需偶尔审查。

这并不意味着传统编程语言设计不再引人入胜，而是设计的权衡与以往大不相同。Rust的使命依然清晰：足够底层以编写内核，足够高层以构建应用。围绕Agent的演进意味着可以容忍一定程度的噪音——比如显式调用clone或share绝不能太多，因为我们仍希望代码的常规路径清晰明了。结合性能分析工具，你会获得一个高效的反馈循环，让代码运行得更快。

证明系统与定理证明器、类型系统之间的关系可以理解为强度与成本的连续谱。类型系统是自动化程度最高、代价最低的一类证明：开发者只写代码，编译器自动完成检查。定理证明器则需要人工或用半自动方式编写规格与证明脚本，表达力最强但门槛也最高，适合验证精妙的算法或并发协议。介于两者之间的还有依赖类型、精化类型和契约式设计，它们允许在类型或注解中嵌入更精细的性质，由求解器自动或半自动验证。三者并非互相取代：类型系统负责廉价而广泛地排除常见错误，证明系统负责对少数关键模块给出严格保证，而证明的产物本身又可以被Agent当作约束条件来生成和修改代码。理解这一分层，才能理解作者为何坚持有了证明系统仍然绝对需要类型系统。