工程哲学：Edsger Dijkstra，优雅并非可有可无

核心要点

• 优雅并非可有可无。 在 Dijkstra 看来，简洁是正确性的前提，而不是达成正确之后才领取的奖赏——无法彻底理解的东西，就无法被证明。
• 证明胜过测试。 “测试只能证明缺陷存在，不能证明缺陷不存在。”对正确性的信心，来自对程序的推理，而绝非来自不断累积的通过用例。
• 先思考，再编码。 他设计最短路径算法时不用纸笔，逼着自己把它压缩到能装进一个人脑子里——正是这种约束催生了优雅。
• 写作即思考。 EWD 手稿全部用钢笔手写、没有撤销键，论证要么在墨水里站得住，要么当场失败——同样的纪律也贯穿于他的文字。

核心原则

“简洁是可靠性的前提。” —— Edsger W. Dijkstra，据传（约 1975 年）¹

这句话作为一句格言流传下来，几乎像一条页边批注，与他 1975 年前后那些故意带有挑衅意味的备忘录相关联。脱离了语境，它读起来像一句口号，但 Dijkstra 是把它当作一个严格的逻辑论断来说的。可靠性不是靠更狠地测试就能添加到一个复杂系统上的东西。一个你无法彻底理解的系统，就是一个你无法证明其正确的系统；而一个你无法证明其正确的系统，终将以你未曾预料的方式失败。简洁不是一种与正确性相互竞争的审美偏好，它是正确性赖以构建的材料本身。没有前者，就别想拥有后者。

这与大多数软件实际的写法恰好相反。人们的常见本能是：先把东西做出来、跑通，然后不断测试，直到缺陷不再冒头——把简洁当作日后若有余力再去追求的奢侈品。Dijkstra 毕生的事业，就是论证这个顺序既颠倒又危险。他被引用得最多的那句话，正是由此直接推出的警告：“测试只能证明缺陷存在，不能证明缺陷不存在。”²一个通过的用例，对你没有尝试过的那些输入只字未提。要确知一个程序没有缺陷，唯一的办法是对它进行推理——而你只能对足够简单、能装进一个人脑子里的东西进行推理。对 Dijkstra 而言，优雅“不是可有可无的奢侈品，而是一个往往决定成败的因素”。³

正是这一信念，使他立于本系列的源头。Linus Torvalds 会不断重塑一个问题，直到特例消失不见，John Carmack 则把问题剥到只剩下高速运转的内核，而 Dijkstra 提供了二者共同继承的那个根本论断：优雅的解和正确的解，是同一个解。这是把品味当作一套技术体系、而非审美上的放纵来对待的最初论据——也是早在有人给它命名之前数十年，就主张以证明取代貌似合理的论据。

背景

Edsger Wybe Dijkstra 于 1930 年 5 月 11 日生于荷兰鹿特丹，2002 年 8 月 6 日逝于纽嫩。⁴他的父亲是一位化学家，曾任荷兰化学学会会长；他的母亲是一位数学家，据他自己说，她对一个数学论证何时优雅、何时只是恰好奏效有着异乎寻常清晰的判断力。他在莱顿大学攻读数学与理论物理，随后于 1952 年到阿姆斯特丹的数学中心从事编程工作——当时“程序员”还算不上一种受认可的职业。据说 1957 年他想在结婚证上把它登记为自己的职业时，荷兰当局拒绝接受，因为官方根本不存在这样一种工作；他只好改写成“理论物理学家”。⁴

这个细节并非趣闻轶事。Dijkstra 此后毕生坚持，编程是一门严谨的智力学科，而非一项文书性的手艺；而这种坚持，早在这门学科有名字之前就开始了。他先是在数学中心任职，1962 年成为埃因霍温理工大学的教授，整个 1970 年代担任 Burroughs 公司的研究员，并于 1984 年出任德克萨斯大学奥斯汀分校 Schlumberger 计算机科学百年讲席教授，直至 1999 年退休。⁴

1972 年，他获得 ACM 图灵奖。授奖词值得全文一读，因为它对这一原则的概括胜过任何摘要：“表彰其对作为一项崇高智力挑战的编程所做的根本性贡献；表彰其雄辩地坚持并切实地证明，程序应当被正确地构造出来，而非仅仅靠调试得出正确；表彰其在程序设计基础问题上富于洞见的认识。”⁵被正确地构造出来，而非仅仅靠调试得出正确。 这句话，就是这个人的全部。

主要工作

最短路径算法（1956 年构思，1959 年发表）

1956 年，有人请 Dijkstra 找一个能在新机器 ARMAC 正式启用仪式上一展身手的问题——要让非技术背景的观众也能跟得上。他选了荷兰 64 座城市中任意两座之间的最短路线，因为人人都能听懂这个问题、也能核对答案。这个解法降临到他身上的方式，是他百说不厌的：“一天上午，我和年轻的未婚妻在阿姆斯特丹购物，累了，便在咖啡馆的露台坐下喝一杯咖啡，我正想着自己能不能解出这个问题，于是就设计出了求最短路径的算法。”⁶前后大约花了二十分钟。

他得出它的方法，才是这里的教益所在。“它之所以如此漂亮，”他后来说，“原因之一是我设计它时没用纸笔。我后来才明白，不用纸笔设计的好处之一，是它几乎逼着你去避开一切可以避免的复杂。”⁶他无法依赖草稿，于是这个想法必须小到能完整地装在脑子里。约束催生了优雅。他三年后才把它发表出来——1959 年那篇刊于 Numerische Mathematik 的论文《A Note on Two Problems in Connexion with Graphs》篇幅勉强超过一页——因为照他的说法，编程在当时还算不上一项体面到值得撰文论述的活动。⁶

这个算法是贪心的：它总是先扩展最近的、尚未访问的节点，形成一道不断扩张的波前，依次以最短距离抵达每一个点。它简单到可以在咖啡桌旁讲清楚，而且可被证明是最优的——波前第一次触及目标时，那条路径无人能及。简单与正确，在这里并不冲突。它们是同一个事实。

《Go To 语句有害论》与结构化编程（1968 年）

1968 年，Dijkstra 向 Communications of the ACM 投了一封信，题为《A Case Against the Goto Statement》。编辑 Niklaus Wirth 把它改名为《Go To Statement Considered Harmful》——这个说法催生出一整套效仿的文章体裁，如今比信中任何内容都更出名。⁷ Dijkstra 的论证不是一份风格指南，而是认识论层面的。不加约束的 goto 允许控制流跳到任何地方，这意味着要弄清一段程序在某一行正在做什么，你可能不得不追踪所有可能导向该行的路径。程序的文本与程序的行为就此脱节。而在结构化的控制流下——顺序、选择和循环——文本与执行始终保持对应，你读一个代码块，就能对这个代码块进行推理。

这个论证与最短路径中的那条约束是同一个原则，只是被应用到了语言设计上：把东西保持得小到足以推理。结构化编程并不是要禁用某个关键字，而是要保住人类“通过阅读来证明程序正确”的能力。图灵奖授奖词里点名的那一连串他的词汇——“死锁拥抱”（deadly embrace）、“信号量”（semaphore）、“无 goto 编程”、“结构化编程”——正是一份记录，记下了他如何彻底重塑了程序员思考所用的语言。⁵

他在操作系统上的工作也带着同样的基因。THE 多道程序系统（1968 年）被构建为严格分层的抽象层级，每一层都可以独立验证。为协调并发进程，他发明了信号量及其 P、V 操作；他还把哲学家就餐问题塑造成关于死锁与饥饿的教学式提炼——一个被压缩到能装进脑中的艰深并发问题。⁴⁵后来又有了自稳定，以及《A Discipline of Programming》（1976 年）中的谓词转换器 / 最弱前置条件演算：一种把程序和它的正确性证明手拉手一并推导出来的方法，而不是先写代码、再指望事后去验证它。⁴⁵

谦卑的程序员：证明高于测试（1972 年）

Dijkstra 的图灵奖演讲《The Humble Programmer》（EWD340），是关于“为何简洁是一种道德关切、而不仅仅是实用考量”的最清晰陈述。它的核心论断，关乎人脑的尺寸。“称职的程序员充分意识到自己头骨严格有限的容量；因此他以十足的谦卑去面对编程任务，并且尤其会像躲避瘟疫一样躲避那些花哨的小聪明。”⁸聪明并不是一种美德。它是一场赌注——赌你脑中能装下的比实际能装下的更多，而这场赌局会在生产环境里见分晓，且赌的是你输。

这篇演讲落脚于一条堪称“构造即正确”软件立身宪章的主张：“只要我们带着对编程任务那巨大难度的充分体认去面对它，只要我们坚守朴素而优雅的编程语言，只要我们尊重人脑固有的局限、以非常谦卑的程序员的姿态去面对这项任务，我们就能把编程这件事做得好得多。”⁸在这个框架里，测试从根本上是不充分的——并非因为测试无用，而是因为它至多只能对输入空间进行采样。他这一警告的经典完整表述，出自《Notes on Structured Programming》，毫不含糊：“程序测试可以用来证明缺陷的存在，但绝不能用来证明缺陷的不存在！”⁹若你想要的是缺陷的不存在，就必须去证明它，而你只能证明你所能理解的东西。

作为一种实践的 EWD 手稿（1960 年代—2002 年）

在大约四十年间，Dijkstra 写下了一系列编号的手稿——备忘录、证明、行程报告、随笔与论辩——一律以他的姓名首字母“EWD”为前缀。这个系列一直编到 EWD1318，实际文档超过一千份；编号多于文档数，是因为他在开始动笔时就分配一个号码，而并非每一篇都最终完成。⁴¹⁰其中绝大多数都是用一手以精准著称的字迹、以钢笔手写而成。他不在计算机上起草。他会写好一份手稿，复印，再寄给一小圈同行，这些人再复印、再转寄出去——一种前互联网时代的“地下传抄”，让 EWD 系列的影响力远远超出“几乎没有一篇正式发表过”这一事实所应有的程度。⁴¹⁰完整系列如今已扫描，在 UT 奥斯汀的 E.W. Dijkstra 档案馆中免费提供。¹⁰

这种实践与那套哲学密不可分。慢慢地手写、没有撤销键，逼出的正是与不用纸笔设计算法相同的纪律：你无法靠堆量或反复修改来藏拙。一个论证要么成立，要么不成立，而你要用墨水对它做出承诺。EWD 系列展示的，正是一位工程师把写作本身当作清晰思考的工具、并把清晰本身视为全部目的时，会是什么模样。

方法

这套方法，是一个信念在四十年间被持之以恒地反复施行。

把它做到足够小，小到能够推理。 咖啡馆里的那个算法、结构化的控制流、分层的 THE 系统、哲学家就餐的提炼——每一项都是把一个问题不断缩小、直到人脑能容下它的全部并加以核对的行动。你无法通览的复杂，就是你无法信任的复杂。

去证明，而不是去测试。 测试是采样；证明是认证。Dijkstra 的谓词转换器演算之所以存在，是为了让证明与程序被一并推导出来，而不是先写好一个、再把另一个硬拼上去。“被正确地构造出来，而非仅仅靠调试得出正确”——这套方法，五个字就道尽了。⁵

把优雅当作证据，而非装饰。 当一个解法丑陋时，那份丑陋通常是一个信号，表明问题尚未被理解。优雅之所以“决定成败”，是因为优雅的形态正是出错之处最少的那一种。³

为思考而写。 EWD 系列不是工作完成之后产出的文档。它们本身就是工作——被化为可见的推理，承载于一种容不得含糊其辞的介质之中。不用纸笔去设计，再把结果用钢笔郑重写下，是同一种纪律施行了两遍。

影响脉络

谁塑造了他

他的母亲，那位数学家。 Dijkstra 把自己对数学优雅的感受力归功于她——那种对“一个证明何时不只是有效、而且干净”的训练有素的直觉。这一区分——一个奏效的论证与一个优美的论证之间的区分——成了他整个生涯的轴心。（成形期影响）

Algol 60 项目。 Dijkstra 参与构建了最早的 Algol 60 编译器之一，这门语言的块结构与递归为他的结构化编程提供了原材料。Algol 是一个证明：一门编程语言可以为清晰而设计，而不是为便利而层层堆积。（直接影响）

数学的证明传统。 在“计算机科学”尚不存在之前，Dijkstra 受的是数学家与物理学家的训练，他把证明这一标准原封不动地引入进来。在他看来，程序是一个数学对象，要问的从来不是“它看上去能用吗？”，而是“你能证明它必定能用吗？”（成形期影响）

他塑造了谁

每一个写结构化代码的程序员。 goto 从日常编程中销声匿迹、顺序/选择/迭代的普遍通行，以及整套并发词汇——信号量、死锁、互斥——都是他的遗产，无形地运转在此后写下的每一份代码里。

形式化方法与程序验证。 谓词转换器演算与“构造即正确”的理想，是现代验证、模型检验和携带证明的代码的直接祖先。当下形式化验证系统软件的复兴，正是 Dijkstra 的论断终于遇上了快到足以运行它的硬件。

这门学科的自我形象。 比起任何具体的成果，Dijkstra 更确立了这样一个观念：编程是应用数学的一个分支，配得上严谨——而不是一门靠反复试错学来的手艺。这个领域的良心，无论好坏，至今仍以他的腔调发声。

贯穿始终的主线

Dijkstra 是本系列其余部分由之流出的源头。Linus Torvalds 所说的“好品味”——那次让特例消失的重写——正是 Dijkstra 的“简洁即正确”在一位内核黑客口中的说法：分支越少，出错之处就越少。John Carmack 那个高速、简单的内核，是同一种减法，只不过瞄准的是硬件的天花板，而非证明。而 Andrej Karpathy 坚持从零重建一个系统、以求真正理解它，则是 Dijkstra 的“不用纸笔去设计”戴上了一顶深度学习的帽子。这四个人几乎在所有事情上意见相左，唯独在那件最要紧的事上一致：优雅的结构不是叠加在正确的解之上的。它就是正确的解。（系列衔接）

我从中得到的

我反复回到的那句话，是那个倒转：简洁是可靠性的前提，而不是你达成可靠之后才领取的奖赏。大多数又慢又脆的软件之所以又慢又脆，不是因为有人省略了测试，而是因为从来没有人把它做到足够小、小到能够理解，于是没有人能对它进行推理，于是唯一可用的质量策略就只剩下“一直测到看得见的缺陷不再出现”——而正如 Dijkstra 所说，这什么也证明不了。这个倒转，与质量是唯一的变量是同一条标准：要问的从来不是“测试通过了吗？”，而是“我对它的理解，是否足以确知它是正确的？”

在我如今所构建的世界里——AI 代理、工具循环、生成代码的速度超过任何人阅读速度的系统——Dijkstra 的警告比以往任何时候都更为尖锐。当一个代理写下上千行代码、而测试一片绿时，那正是他所描述的处境：缺陷的存在未被证明，而它们的不存在也无法被证明。Dijkstra 式的做法，是拒绝让“理解”随着“生成”的扩张而缩小——是坚持让系统保持足够小、足够分层、足够可读，好让仍有人能证明它是对的。正因如此，即便没有人阅读代码，我也把验证层当作承重结构来对待：测试证明存在，而非不存在；而一整片绿色的对勾，并不是一个证明。

常见问题

Edsger Dijkstra 的工程哲学是什么？

Dijkstra 认为简洁是可靠性的前提：一个程序必须简单到人能彻底理解，因为只有可理解的程序才能被推理、被证明正确。他主张程序应当“被正确地构造出来，而非仅仅靠调试得出正确”，主张测试可以证明缺陷的存在却绝不能证明其不存在，并主张优雅不是装饰，而是“一个往往决定成败的因素”。在他看来，聪明是一种恶习，因为它超出了人脑有限的容量。³⁵⁸⁹

Edsger Dijkstra 发明了什么？

Dijkstra 发明了以他名字命名的最短路径算法（1956 年构思，1959 年发表），引入了用于协调并发进程的信号量与 P/V 操作，构建了分层的 THE 多道程序系统，提出了哲学家就餐问题，推进了结构化编程，开创了分布式系统中的自稳定概念，并发展出谓词转换器 / 最弱前置条件演算，用以把程序与其正确性证明一并推导出来（见《A Discipline of Programming》，1976 年）。他于 1972 年获得 ACM 图灵奖。⁴⁵

“测试只能证明缺陷存在，不能证明缺陷不存在”是什么意思？

它的意思是：一个测试只能通过触发缺陷来证明缺陷的存在——它永远无法证明不存在任何缺陷，因为没有任何有限的测试集合能覆盖每一种可能的输入。Dijkstra 在 1969 年的 NATO 软件工程会议上提出了这一观点，并在《Notes on Structured Programming》中给出了经典的完整表述：“程序测试可以用来证明缺陷的存在，但绝不能用来证明缺陷的不存在！”他的结论是：对正确性的信心必须来自证明、来自把程序设计得简单到足以推理，而不是来自不断累积的通过用例。²⁹

Dijkstra 为何手写、并以复印方式传阅 EWD 手稿？

EWD 系列是 Dijkstra 在大约四十年间写下的一千余份编号手稿，其中绝大多数用钢笔手写，随后复印并寄给一小圈人，由他们再复印、再转寄出去。慢慢地手写、没有撤销键，强制施行的正是与他“不用纸笔设计算法”的习惯相同的纪律：它逼出清晰、容不得含糊其辞，因为一个用墨水写定的论证必须真正站得住。完整系列已存档，在德克萨斯大学奥斯汀分校免费提供。⁶¹⁰

参考来源