我第一个经过验证的命令式程序
Hacker News 摘要原标题：My first verified imperative program
这篇文章由Markus Himmel撰写，讨论了即将发布的Lean 4.22版本中全新验证基础设施的特点，重点展示了如何对命令式程序进行性质证明。
文章开头定义了一个具体的编程任务，目的是判断一个整数列表中是否存在两数之和为零的数对。例如，对于列表 [1, 0, 2, -1]，结果为true，因为1与-1相加为0。相对地，列表 [1, 0, -2] 的结果为false。文中展示了一种高效的解决方案，通过遍历列表并使用集合数据结构来追踪已经遇到的元素，以此判断是否存在满足条件的数对。使用哈希集合和二叉搜索树可以实现线性或对数复杂度的效率。
尽管Lean主要是一种函数式编程语言，但它有良好的命令式编程支持。文中展示了如何在Lean中使用局部命令式编程来实现上述算法，代码结构相对直观，使得在该框架下编写程序变得容易。
Lean不仅是编程语言，它还是一个交互式定理证明器。文章中提到，传统上证明局部命令式程序的性质相对困难，因此更倾向于使用函数式风格。而Lean 4.22引入的新框架Std.Do，旨在使验证命令式编程（包括局部和全局）变得简单。本章介绍了Hoare三元组的概念，这是用于判定命令式程序性质的重要工具。
接下来的部分中，Markus展示了如何使用Lean描述函数pairsSumToZero的正确性属性，并介绍了通过mvcgen生成验证条件的过程。此外，作者提到需要为循环提供一个循环不变式（loop invariant），以确认在循环过程中的状态保持一致性。
一旦提供了环不变式，Lean会要求证明五个条件，以确保逻辑的正确性。作者说明了如何通过最新的grind战术快速完成这些"显而易见"的证明工作。
最后，Markus对Lean的设计哲学表达了自己的看法，强调Lean的交互式证明机制与自动化证明确保了程序的可验证性，更加强调了Lean在真实世界程序验证任务中可靠性的重要性。同时，文章也简要介绍了用函数式方式实现的pairsSumToZero函数如何进行验证，展现了函数式编程的简洁性和优雅性。
整篇文章深入探讨了Lean在命令式程序验证中的应用与优势，展示了Lean如何通过直观的语言设计与强大的证明工具，使得复杂的程序逻辑验证变得更加可行和高效。
原文：https://markushimmel.de/blog/my-first-verified-imperative-program/