LLM 无法证明你的代码正确，但它们可以撰写实现证明的样板代码
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
2 posts
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
Literate programming 承诺单一事实来源，但手动的 weave 和 tangle 步骤会破坏 CI/CD 流水线。以下是如何自动化提取和文档生成，使 Markdown 文件保持规范。
如果你的构建流水线必须等你打开终端输入 才能运行，那你就没有文学化程序。你有的只是一本绑着编译器的日记。 文学化编程的全部意义在于散文和代码共享单一事实来源。Markdown 文件就是产物。其他一切——可执行源码、渲染后的文档、测试文件——都是派生的。派生产物属于 CI，不属于你的工作记忆。 问题不是 CI 能不能…