2005 Peter Naur —— ALGOL 60 報告的總編輯與「程式設計即理論」#

「語言的規格寫得再清楚，兩個團隊讀完還是做出不同系統。 Naur 的結論震撼：程式設計的知識無法被文件完整承載。」

案件檔案#

前因#

1958–60 年，國際 ALGOL 委員會要設計「放諸四海皆準」的 科學語言。謎題：如何讓一份文件成為無歧義的合約？ 丹麥天文學家出身的 Naur 接下編輯重責。

線索與推理#

線索一：ALGOL 60 報告（1960）—— 規格的文藝復興#

Naur 以 Backus 的記法（1977 案）為骨架，做出三項革命：

1. BNF 完整形式化語法（後稱 Backus–Naur Form—— Naur 的名字因編輯此報告而被冠上）
2. 刻意不定義實作相關細節（I/O、精度）——語言與 機器脫鉤，可攜性的哲學起點
3. 文本本身就是第一份「正式規格書」的典範——

Knuth 稱之：「程式語言史上劃時代的文件。」

ALGOL 60 雖然商業上失利，其遺傳密碼（區塊、作用域、 遞迴、begin-end、賦值符 :=）遍布 Pascal、C、Java 至今。

線索二：1985 年《Programming as Theory Building》#

Naur 的遲來炸彈：程式不是程式碼，而是團隊腦中的 理論（theory）——對「系統要解決什麼、為什麼這樣解」 的共享理解。推論：

1. 程式碼不能「重建」團隊理論 → 文件不是解藥
2. 修改程式者必須擁有理論 → 外包維護註定品質下降
3. 理論隨人離職而亡 → 人員穩定 > 文件完備

此主張與 Brooks（1999 案）的本質複雜性、敏捷宣言 （2001 年，同一年！）高度共振。

線索三：合成程式設計（Synthetic Programming）#

Naur 晚年批評數學化形式驗證的局限：證明只能約束 「形式面」，無法保證「理論面」正確——規格寫錯了， 證明只會更快地做錯事。他主張以觀察與實驗對待軟體 （近乎科學哲學的立場）。

理論評析#

本案的張力是形式主義 vs 理論建構主義：

歷史判決：兩者並存——模型檢查（2007 案）工業化的同時， code review、pair programming（人的理論傳遞）同樣 不可或缺。

後果#

• 「規格文件」文化、語言標準 ISO 流程的樣板。
• 2020s 的 AI 輔助編程反彈出「理解權」討論：讀不懂 程式碼的團隊，正是 Naur 所謂「失去理論」的團隊。

關聯案件#

→ 1977-John-Backus與FORTRAN高階程式語言、1966-Alan-Perlis與高階程式設計及編譯器、1999-Frederick-Brooks與System360及軟體工程