工程哲學：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 日卒於 Nuenen。⁴ 他的父親是化學家，曾任荷蘭化學學會會長；母親是數學家，據他自己所說，對於一個數學論證何時優雅、何時只是勉強成立，有著異常清晰的感受力。他在萊頓大學攻讀數學與理論物理，接著於 1952 年到阿姆斯特丹的數學中心擔任程式設計的工作——當時「程式設計師」還不是一個被認可的職業。據說 1957 年他在結婚證書上試圖把它登記為自己的職業時，荷蘭當局不予受理，因為官方根本沒有這個職業；他只好改填「理論物理學家」。⁴

這個細節並非花絮。Dijkstra 此後一生都堅持：程式設計是一門嚴謹的智識學問，而不是一種文書匠活；而這份堅持，早在這門學問還沒有名字之前就開始了。他先在數學中心任職，1962 年成為埃因霍溫理工大學教授，1970 年代擔任 Burroughs 公司的研究員，1984 年出任德州大學奧斯汀分校的 Schlumberger 百年講座電腦科學教席，直到 1999 年退休。⁴

1972 年，他獲頒 ACM 圖靈獎。這份頒獎詞值得完整一讀，因為它比任何摘要都更精準地點出了那項原則：「表彰其對於將程式設計提升為一項崇高智識挑戰的根本貢獻；對於『程式應被正確地組構，而非僅靠除錯硬湊出正確』這一主張的雄辯堅持與實際示範；以及對程式設計根基處諸般問題的洞見。」⁵ 正確地組構，而非僅靠除錯硬湊出正確。 這一句話，就是這個人的全部。

主要成就

最短路徑演算法（1956 年構思，1959 年發表）

1956 年，Dijkstra 受託找一個問題，好在 ARMAC 新電腦的正式啟用典禮上展示——某個非技術觀眾也能跟上的東西。他選了 64 座荷蘭城市中兩座之間的最短路線，因為任何人都看得懂這個問題、也驗證得了答案。這個解法是以一種他百說不厭的方式浮現的：「一天早上，我和年輕的未婚妻在阿姆斯特丹逛街，逛累了，就在咖啡館的露台坐下喝杯咖啡，我正想著自己能不能做到這件事，然後我就設計出了最短路徑的演算法。」⁶ 大約只花了二十分鐘。

他找到它的方法，才是真正的功課所在。他後來說：「它之所以這麼漂亮，原因之一，就是我在沒有紙筆的情況下設計出它的。後來我才明白，不用紙筆設計的好處之一，是你幾乎被迫避開一切可避免的複雜。」⁶ 他無法仰賴草稿，所以這個想法必須小到能完整放進他的腦中。是約束催生了優雅。他過了三年才把它發表——1959 年那篇〈A Note on Two Problems in Connexion with Graphs〉刊於《Numerische Mathematik》，篇幅勉強多過一頁——因為照他的說法，當時程式設計還沒被視為值得寫成論文的正經活動。⁶

這個演算法是貪婪的：它永遠優先擴展最近的、尚未造訪的節點，一道不斷擴張的波前，依序以最短距離抵達每一個點。它簡單到能在咖啡桌邊講清楚，而且可被證明為最優——波前第一次觸及目標時，那條路徑無人能勝。在這裡，簡單與正確並不彼此拉扯。它們是同一件事實。

〈Go To 陳述式有害論〉與結構化程式設計（1968 年）

1968 年，Dijkstra 向《Communications of the ACM》投了一封信，標題是〈A Case Against the Goto Statement〉。編輯 Niklaus Wirth 把它改題為〈Go To Statement Considered Harmful〉——這個說法催生了整整一個模仿的文類，如今比信中任何內容都更有名。⁷ Dijkstra 的論點並不是一份風格指南，而是認識論上的。不受約束的 goto 讓控制流可以跳到任何地方，這意味著：要理解一支程式在某一行究竟在做什麼，你可能得追蹤所有可能通往那一行的路徑。程式的文本與程式的行為就此分家。有了結構化的控制流——序列、選擇與迴圈——文本與執行之間保持對應，你只要讀一個區塊，就能對那個區塊進行推理。

這個論點與最短路徑那項約束是同一條原則，只是套用在語言設計上：把東西保持得夠小，才推理得了。結構化程式設計談的不是禁用某個關鍵字，而是要保住人類「藉由閱讀來證明程式正確」的能力。圖靈頒獎詞中那串點名他的詞彙——「致命擁抱」「號誌」「無 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 系列的影響力遠遠超出了「幾乎沒有一篇正式發表」這個事實。⁴¹⁰ 完整系列如今已掃描，並在德州大學奧斯汀分校的 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 在大約四十年間寫下的逾千份編號手稿，多數以鋼筆親手寫成，然後複印、寄給一小圈人，這些人再複印並往外轉寄。緩慢地、沒有復原鍵地親手書寫，逼出了與他「不用紙筆設計演算法」習慣相同的紀律：它逼出清晰、懲罰含糊其辭，因為一個用墨水寫定的論證，必須真的站得住腳。完整系列已存檔，並在德州大學奧斯汀分校免費公開。⁶¹⁰

參考來源