文本编辑器让你写无效代码。树编辑器不会
每个编译器都将你的代码视为树，但你的编辑器让你编辑原始文本。以下是结构化编辑的实际样子、为什么它没有占领市场，以及如何在不更换工具的情况下借用其优势。
每种编程语言都有形式语法。编译器读取它，构建解析树，拒绝任何不符合的内容。编辑器完全无视语法，让你想输入什么就输入什么。 这种脱节是大量摩擦的惊人来源。自动补全建议的标识符在上下文中毫无意义。语法高亮在重构中途崩溃。编辑器眼睁睁看着你犯错，然后报出「Unexpected…
想法与洞见
探索 AI 优先开发、编码护栏和可处置架构。
Donald Knuth希望程序读起来像文学作品。编译器另有打算。
Literate programming承诺代码应该首先为人类编写，其次才是为机器。四十年后，几乎没有人这样写。以下是软件文档化中最优雅的理念为何未能改变我们工作方式的原因。
1984年，Donald Knuth发表了一篇提出根本性反转的论文。程序不应该是为编译器编写、为人类添加注释的。它们应该被写作为人类的文学作品，编译器从中提取可执行部分。他称之为literate programming，并以这种方式构建了TeX。 这个想法很美。它在现代软件开发中也几乎完全缺席。…
修复缺陷是容易的部分。弄清楚它为什么存在才是重要的
大多数团队修复缺陷后就继续前进。同样的缺陷反复出现。以下是如何在费根审查内部运行因果分析，从而停止两次编写同样的缺陷。
每个团队都有一个反复出现的缺陷。分页中的差一错误。认证中间件中缺失的空值检查。三个冲刺前有人「修复过」的结账竞态条件。 你并不是三次写了同一个缺陷。你写了三个具有相同原因的不同缺陷。修复处理的是症状。原因依然隐藏。…
Pull Request 审查能发现 15-30% 的缺陷。数据 50 年前就已给出答案。
IBM、AT&T、HP 和 Microsoft 的多项研究均证实，非正式代码审查大约能发现四分之一的缺陷。以下是数据实际说明的内容、该比例偏低的原因以及解决方法。
非正式代码审查能够发现被审代码中 15% 到 30% 的缺陷。这不是观点，而是在四十年、多家公司、数十项研究中反复验证的结论。 迈克尔·费根于 1976 年在 IBM 记录了这一数据。1987 年 AT&T 贝尔实验室的研究发现了 20%。1996 年惠普的研究发现了 25%。2013…
通用检查清单什么都抓不到。结构化检查清单能发现60%的缺陷。
大多数审查检查清单都是复制粘贴的良好愿望列表。Fagan inspection风格的结构化检查清单基于实际缺陷数据构建，针对特定工件类型，并在个人准备阶段使用。以下是如何构建一个有效的检查清单。
如果你的团队有一份代码审查检查清单，它很有可能躺在没人打开的维基页面上。上面大概写着"check for off-by-one errors"和"verify error handling"之类的话。这些话都是对的。但也过于笼统，不足以改变行为。 一份告诉你"check for…
大语言模型可以预先审查你的代码，但它无法主持会议
费根审查需要四到六个人、两小时才能审完250行代码。大语言模型可以通过承担准备工作和检查清单的执行来削减这部分成本，但它无法取代人类角色去发现最昂贵的缺陷。
一次完整的费根审查需要一名主持人、一名朗读员、两到四名审查员，以及作者本人。团队以每小时125行的速度，花费两小时审查大约250行代码。这意味着一次小小的改动就要消耗八到十二人时。 大语言模型可以在不到一秒内读完250行代码。它可以执行检查清单、标记可疑模式，并在任何人打开文件之前就生成一份结构化的缺陷记录。…
Fagan Inspections 在测试前发现90%的缺陷。然后我们不再使用它。
Michael Fagan 在 IBM 设计的结构化审查流程，能在代码进入编译器之前捕获几乎全部缺陷。但它也消耗了项目总工时的15%–20%。本文解释软件史上最有效的审查方法为何消失，以及团队究竟失去了什么。
1976年，Michael Fagan 在 IBM Systems Journal 上发表了一篇论文，描述了一种审查流程，其有效性使之成为软件质量的金标准。Fagan Inspections 在尚未运行任何测试之前，就能捕获全部缺陷的60%到90%。NASA…
你最优秀的审查员也会遗漏大多数缺陷。Fagan 于1976年在IBM测量了这一点。
即使是高级工程师，在非结构化审查中也只能发现一小部分缺陷。Michael Fagan 在IBM的研究揭示了原因，并构建了结构化审查流程来解决这一问题。
两位高级工程师审查同一份拉取请求。一位标记了缺失的空值检查。另一位发现了清理路径中的竞态条件。两人都没有发现全部问题。 如果你只指派了一位审查员，那么其中一个缺陷就会被发布上线。这不是技能差距。这是人类注意力的可预测特性，而 Michael Fagan 于1976年在IBM记录了这一现象。 Fagan…
大多数代码审查只能发现20%的缺陷。Fagan Inspection能发现90%。
非正式的代码审查只能发现15%到30%的缺陷。Fagan Inspection是一种有50年历史的结构化流程，持续报告60%到90%的缺陷移除率。以下是它的工作原理、团队回避它的原因，以及如何运行轻量级版本。
大多数代码审查只能发现本应找到的缺陷的15%到30%。这不是猜测。IBM在20世纪70年代就测量过，AT&T、惠普和微软的研究也在数十年间反复确认了这一范围。 非正式审查成本低廉、异步进行、 socially…
AutoVerus将40小时的证明编写变成3次LLM调用。诀窍在于知道何时放弃。
AutoVerus利用LLM智能体网络为Rust代码生成Verus正确性证明，通过由SMT求解器反馈驱动的生成-修复-消除循环，自动化超过90%的证明义务。
形式化验证中最困难的部分从来不是验证器本身，而是编写证明。 给一位资深Rust工程师Verus——微软研究院开发的基于SMT的验证器——他可以在一个下午内为函数添加前置条件和后置条件注释。然后验证器会以机械确定性告诉他，该函数是否对所有可能的输入满足这些契约。这部分令人满意。…