LLM 无法证明你的代码正确，但它们可以撰写实现证明的样板代码
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
想法与洞见
探索 AI 优先开发、编码护栏和可处置架构。
Cleanroom 实现每千行 0.1 个缺陷。你不需要全盘照搬也能达到这个目标。
Cleanroom software engineering 将 defect rate 降低 100 倍，但全面采用需要独立的 test team 和 formal proof。这里介绍一种 pragmatic subset，无需 overhead 即可捕获大部分收益。
Cleanroom software engineering 每千行代码仅产生 0.1 个缺陷。业界平均水平是 10 到 50。问题是，完整的 Cleanroom 要求你将团队拆分为 author 和 verifier，在每个 module 之前编写 formal specification，并禁止…
IBM 的 Zero-Defect Process 实现了每 KLOC 0.1 个 Bug。行业还是抛弃了它。
IBM 的 Cleanroom engineering 达到了比行业平均水平好 100 倍的 defect rate，然后消失在历史中。它的消失与是否有效毫无关系。
IBM 的 Cleanroom software engineering process 实现了每千行代码 0.1 个 defect。当时的行业平均水平在 10 到 50 之间。该 process 被文档化，在多个项目和语言之间 replicate，并经过独立验证。然后它消失了。 不是因为更好的 method…
真的有人验证了 1 万行代码零缺陷吗？IBM 做到了，而且方法比结果更离奇。
Cleanroom software engineering 承诺通过 mathematical verification 而非 debugging 实现零缺陷增量。我们查看 IBM 的实际项目数据，看看这一说法是否成立。
1980 年代软件行业的平均水平是每千行代码 30 到 60 个缺陷。IBM 的 Cleanroom 团队交付了一个 2 万行的编译器增量，在测试中发现了 53 个缺陷。也就是每 KLOC 2.6 个。一些 1 万行的独立增量在进入系统测试时，没有发现任何缺陷。 最离奇的部分？程序员被禁止运行自己的代码。…
你的模块有三层。你可能只写了一层。
Box Structure 强制你将模块的行为、记忆的状态和实现方式定义为三个独立且可验证的层。以下是 Cleanroom 如何利用它们消除调试。
你先写代码，再写测试，然后发现代码是错的。这是标准循环。也是为什么调试会消耗大多数项目时间线的一半。 Box Structure 把这个过程反转。你在写代码之前就定义行为，用数学方式验证这个定义，然后一层一层翻译成代码。结果是"构造即正确"的模块，而不是"测试碰巧通过所以正确"。…
IBM 禁止开发者运行自己的代码，从而交付了每千行代码 0.1 个缺陷的软件
IBM 的 Cleanroom 工程流程通过预防而非发现缺陷，实现了比行业平均水平好 100 倍的缺陷率。以下是它的工作原理、为何几乎无人使用，以及你今天可以借鉴什么。
IBM 交付了一套 NASA 卫星控制系统，每千行代码仅有 0.1 个缺陷。当时的行业平均水平在 10 到 50 之间。他们并非依靠招聘更聪明的工程师或延长工作时间来达成这一目标。他们靠的是禁止开发者运行自己的代码。 这就是 Cleanroom 软件工程，由 IBM 的 Harlan Mills 于 1970…
你的文学化程序在 CI 能无需你参与就完成 tangle 之前都是坏的
Literate programming 承诺单一事实来源，但手动的 weave 和 tangle 步骤会破坏 CI/CD 流水线。以下是如何自动化提取和文档生成，使 Markdown 文件保持规范。
如果你的构建流水线必须等你打开终端输入 才能运行，那你就没有文学化程序。你有的只是一本绑着编译器的日记。 文学化编程的全部意义在于散文和代码共享单一事实来源。Markdown 文件就是产物。其他一切——可执行源码、渲染后的文档、测试文件——都是派生的。派生产物属于 CI，不属于你的工作记忆。 问题不是 CI 能不能…
先向LLM解释代码，让我的缺陷率降低了85%
我花了30天时间，在向LLM索要代码之前先撰写设计说明。结果改变了我对rubber-ducking的看法。
大多数开发者把LLM用反了。我们用五个词描述需求，拿回200行代码，然后花下一个小时调试模型做出的假设。 我花了三个月时间运行相反的流程：在索要哪怕一行代码之前，先写一份完整的设计说明。结果代码缺陷更少了，但真正的进步在于我自己的理解。 Donald Knuth在1984年提出了"literate…
我把测试、代码和散文都放在一个 Markdown 文件里，再也不用往文档里复制代码了
Literate programming 将 Markdown 文件作为单一事实来源，使文档、测试和实现保持同步。以下是如何用三十行 Python 实现它。
你的文档、测试和代码是三份文件，讲着同一个故事，却讲得都很糟糕。 你在源码里更新了函数签名，忘了改 README 里的示例。一周后，新员工把过时的代码片段复制到了生产环境。你的测试文件仍然把旧的行为编码为预期结果。现在你有两个 bug 和一个文档工单。…
你的 Claude 对话已经是文档了。只是它会在 12 小时后消失。
LLM 对话包含意图、被拒绝的替代方案以及可运行的代码。这正是文档应该包含的内容。以下是将 ephemeral chat 转换为持久、可搜索的文档，同时不丢失叙事的方法。
你花了 45 分钟和 Claude 设计一个 retry circuit。你解释了 failure modes，因为 exponential backoff 会掩盖 cascading pressure 而拒绝了它，确定了 token-bucket rate limiting with…