一个程序员的心路历程
给Rust代码办一张“数学身份证”：亚马逊揭秘Nitro背后的形式化验证武器Verus
Rust 的类型系统能防内存越界和数据竞争，却证明不了“代码算出来的业务逻辑是对的”。本文深度揭秘亚马逊在 AWS Nitro 隔离引擎等核心基础设施中引入的形式化验证利器——Verus。Verus 允许开发者直接在 Rust 源码中嵌入数学规约，依托自动求解器实现秒级证明反馈，甚至能为脱离编译器保护的 unsafe 代码与自定义并发锁建立不可动摇的数学级正确性保证。文章详细拆解了 Verus 的工作流程、“幽灵代码擦除”机制及开源生态的落地现状。
Rust 核心开发者发出“存在主义焦虑”：Agent 写代码的时代，语言设计者还有饭碗吗？
Rust 近期热度飙升，Meta 今年的 Rust 代码量已超过此前 9 年总和。Rust 核心开发者 Niko Matsakis 认为，原因在于 Rust 的“默认高性能”与“类型系统护栏”恰好契合 Agent 编程。本文结合他的文章，以及 Lean 社区的 lean-zip 实验和 AWS 工程师 Marc Brooker 的“反馈回路假说”，梳理 Rust 的优势、局限，以及“证明系统 + 设计语言”这条可能的演进路线。
Claude Code 团队是如何进行代码审查的
在已有 90% 代码由 Claude 自主编写的背景下，Claude Code 团队首次公开了如何解决海量代码审查瓶颈的实战工程体系。面对日均数万次合并的吞吐压力，团队摒弃传统逐行看代码的“人肉把关”，建立起涵盖提 PR 前自验、多 Agent 投票审查、阻断性安全校验、三档动态风险审批以及合并队列的分级防御网。同时，通过引入事故转评测集与轮数硬封顶等收敛机制，团队在 PR 合并量翻倍的同时将回滚率压降超 40%，将人类极其有限的注意力精准锚定在架构决策与业务意图上。
当90%代码由AI写完，程序员社区、编程语言、开发工具将何去何从？
Elixir之父José Valim近日在X发长文《Evolving programming languages in the AI era》，引发大量转发讨论。他认为当AI Agent写掉大部分代码后，编程语言的“人体工学”优化会失去意义，但编译器不会消失；真正该被重新设计的，是IDE、LSP、调试器这些“为人类交互而生”的工具——他提出用可查询的“程序数据库”取代LSP、用运行时可观测性取代传统调试器。本文完整梳理其核心观点及评论区激辩。
Unsafe Rust：当 Rust 的安全边界开始变得模糊
在 RustConf 2026 上，C 标准委员会主席 Robert Seacord 带来了一场精彩的演讲：当 Rust 进军汽车、航天与内核等安全关键系统，Unsafe Rust 的未决（unsettled）语言语义正成为新的工程隐患。文章指出，Rust 不可能消灭 unsafe，而测试通过并不能证明没有未定义行为（UB）；从复杂的指针来源（Pointer Provenance）到别名模型，Rust 当前的核心任务不仅是减少 unsafe，更是依托 Miri、MiniRust、Tree Borrows 等基础设施，为 Unsafe 世界绘制出一张精确、可验证的语言规范地图。