「 Lamport讲座-简报」编码不是编程（Coding isn't Programming）
编码的喧嚣之外：在 Lamport 演讲中重拾编程的本质
内容整理自：图灵奖得主莱斯利·兰伯特（Leslie Lamport）的演讲：“编码并非编程”（Coding isn't Programming）。
兰伯特认为：我们日常所说的“编程”，其核心远不止于敲击键盘、编写代码。他强调，真正的“编程”，是一种在代码诞生之前的智力活动，是一种关乎思考、设计与抽象的过程。而“编码”，仅仅是将这些思考结果转化为机器可执行指令的最后一步。
他坦言，许多从并发编程中获得的教训，实际上适用于所有类型的程序开发。并发程序之所以困难，是因为线程间无数可能的交错执行方式导致了状态空间的爆炸，使得传统的调试方法几乎失效。“你无法确定你检查了所有相关的情况，”他说道，“修复一个 Bug 很有可能引入另一个。” 面对这种复杂性，唯一的出路是在编码前找到一个正确的算法或设计。先有清晰的蓝图，再动手建造。这个原则，他认为，应该推广到所有不那么简单的程序开发中。
这里的关键在于“抽象”。兰伯特认为，我们过于“迷恋语言”本身，而忽略了语言所要表达的更高级别的“思想”。对于一个特定的编程任务，尤其是那些并非标准库算法能直接解决的部分，我们需要构建一个“抽象视图”或“抽象程序”。这是一种比代码更高层次的描述，它关注的是“程序做什么”（What）和“程序如何做”（How），而不是具体的语法细节。
为了说明这一点，他用了一个极其简单的例子——计算数组中的最大元素。一个看似微不足道的任务，却在“空数组”这个边界条件下暴露了初始规范（“What”）的缺陷。传统的做法是添加代码来处理这个特殊情况。但兰伯特展示了另一种更优雅的方式：通过抽象思维。首先，将问题从“整数数组”推广到“数字多重集”，剥离不必要的限制。然后，他运用基础的数理逻辑，重新定义了“What”——不再是找“最大元素”，而是找“大于等于集合中所有元素的最小数字”。这个定义在集合非空时等价于最大值，而在集合为空时，自然地导出了结果 （负无穷大）。这样一来，描述“How”的算法本身就无需为“空集”情况打任何补丁，变得更加简洁和统一。在“What”层面多花时间思考，甚至引入数学的严谨性，能够极大地简化“How”层面的实现复杂度，这在处理远比求最大值复杂的问题时，其价值不言而喻。
那么，如何确保我们设计的抽象“How”是正确的呢？兰伯特指出，仅仅通过测试几个案例是远远不够的，尤其是在非确定性或并发场景下。我们需要证明它对于所有可能的执行都正确。他推崇将程序执行视为一个“状态”（State）的序列，而非仅仅是代码步骤的序列。一个状态包含了所有影响未来执行路径的信息。程序的正确性，则往往依赖于一个或多个“不变量”（Invariant）——即在程序执行的每一个可达状态下都必须为真的属性。
对于那个求最大值的抽象算法，他给出了一个简洁的不变量： （其中 x 是当前找到的候选最大值，B 是剩余待处理元素的集合，A 是原始输入集合）。理解并证明这个不变量（它在初始状态为真，并且每一步执行都保持其为真），是确信算法正确性的关键。如果我们不理解保证程序正确运行的那个不变量，我们就等于不理解这个程序。他甚至略带严肃地提醒，未来，无法进行这种层次思考的程序员，可能会率先被 AI 取代。
这种强调抽象和严谨性的方法并非纸上谈兵。兰伯特引用了亚马逊 AWS 使用他设计的 TLA+ 语言进行系统设计的例子。AWS 的工程师发现，这种方法能够揭示出传统测试手段无法发现的深层设计缺陷，并且具有良好的投资回报率，因为在设计早期修复缺陷的成本远低于后期修改代码。他还提到了欧洲航天局 Virtuoso 操作系统的案例，通过 TLA+ 进行高层设计，新系统的代码量相比前一版本竟减少了十倍之多——这绝非仅仅改进编码技巧所能达到的成就，而是源于更清晰的架构和更高质量的抽象设计。
那么，如何培养这种抽象思考能力？兰伯特认为，“写作是大自然让你知道自己思维有多么马虎的方式。” 思考需要通过书写来使其清晰化、结构化。同时，他也指出了数学教育在培养抽象思维上的核心作用。抽象，正是数学的本质。
我们身处一个追求快速交付、迭代敏捷的时代，但兰伯特提醒我们，有些基础性的东西是不能被速度所取代的。编程的核心在于思考，在于构建清晰、正确的抽象模型。编码只是将这个模型转化为现实的手段。过度关注编码技巧和最新的编程语言，而忽视了前期的深度思考和设计，无异于舍本逐末。
最后，他在补充环节谈及为何程序“应该”有 Bug，进一步点明了问题的关键：现代软件大量依赖缺乏精确规范的库，使得我们甚至无法清晰定义“正确”的行为是什么，自然也就难以判定何为“Bug”。这更加凸显了为软件组件提供清晰、抽象规范的重要性。
“Coding isn't Programming”这句话，是一个定义上的辨析，更是一种对软件开发价值核心的重新定位。在未来的工作中，面对复杂的任务时，或许应当提醒自己：停下敲击键盘的手，先拿起纸笔，像兰伯特所倡导的那样，去思考，去抽象，去构建那个坚实可靠的蓝图。因为，那才是真正的“编程”开始的地方。