想法與洞見

探索 AI 優先開發、編碼護欄和可處置架構。

IBM 的 Zero-Defect Process 實現了每 KLOC 0.1 個 Bug。業界還是拋棄了它。

IBM 的 Cleanroom engineering 達到了比業界平均水準好 100 倍的 defect rate,然後消失在歷史中。它的消失與是否有效毫無關係。

IBM 的 Cleanroom software engineering process 實現了每千行程式碼 0.1 個 defect。當時的業界平均水準在 10 到 50 之間。該 process 被文件化,在多個專案和語言之間 replicate,並經過獨立驗證。然後它消失了。 不是因為更好的 method…

真的有人驗證了 1 萬行程式碼零缺陷嗎?IBM 做到了,而且方法比結果更離奇。

Cleanroom software engineering 承諾透過 mathematical verification 而非 debugging 實現零缺陷增量。我們查看 IBM 的實際專案資料,看看這一說法是否成立。

1980 年代軟體業的平均水平是每千行程式碼 30 到 60 個缺陷。IBM 的 Cleanroom 團隊交付了一個 2 萬行的編譯器增量,在測試中發現了 53 個缺陷。也就是每 KLOC 2.6 個。一些 1 萬行的獨立增量在進入系統測試時,沒有發現任何缺陷。 最離奇的部分?程式設計師被禁止執行自己的程式碼。…

你的模組有三層。你可能只寫了一層。

Box Structure 強制你將模組的行為、記憶的狀態和實作方式定義為三個獨立且可驗證的層。以下是 Cleanroom 如何利用它們消除除錯。

你先寫程式碼,再寫測試,然後發現程式碼是錯的。這是標準循環。也是為什麼除錯會消耗大多數專案時間線的一半。 Box Structure 把這個過程反轉。你在寫程式碼之前就定義行為,用數學方式驗證這個定義,然後一層一層翻譯成程式碼。結果是「構造即正確」的模組,而不是「測試碰巧通過所以正確」。…

IBM 禁止開發者執行自己的程式碼,從而交付了每千行程式碼 0.1 個缺陷的軟體

IBM 的 Cleanroom 工程流程透過預防而非發現缺陷,達成了比業界平均好 100 倍的缺陷率。以下是它的運作方式、為何幾乎無人使用,以及你今天可以借鏡什麼。

IBM 交付了一套 NASA 衛星控制系統,每千行程式碼僅有 0.1 個缺陷。當時的業界平均水準在 10 到 50 之間。他們並非依靠招聘更聰明的工程師或延長工作時間來達成這項目標。他們靠的是禁止開發者執行自己的程式碼。 這就是 Cleanroom 軟體工程,由 IBM 的 Harlan Mills 於 1970…

你的文學化程式在 CI 能無需你參與就完成 tangle 之前都是壞的

Literate programming 承諾單一事實來源,但手動的 weave 和 tangle 步驟會破壞 CI/CD 流水線。以下是如何自動化提取和文件生成,使 Markdown 檔案保持規範。

如果你的建置流水線必須等你開啟終端機輸入 才能執行,那你就沒有文學化程式。你有的只是一本綁著編譯器的日記。 文學化程式設計的全部意義在於散文和程式碼共享單一事實來源。Markdown 檔案就是產物。其他一切——可執行原始碼、渲染後的文件、測試檔案——都是衍生的。衍生產物屬於 CI,不屬於你的工作記憶。 問題不是 CI…

先向LLM解釋程式碼,讓我的缺陷率降低了85%

我花了30天時間,在向LLM索取程式碼之前先撰寫設計說明。結果改變了我對rubber-ducking的看法。

大多數開發者把LLM用反了。我們用五個詞描述需求,拿回200行程式碼,然後花下一個小時除錯模型做出的假設。 我花了三個月時間執行相反的流程:在索取哪怕一行程式碼之前,先寫一份完整的設計說明。結果程式碼缺陷更少了,但真正的進步在於我自己的理解。 Donald Knuth在1984年提出了「literate…

我把測試、程式碼和散文都放在一個 Markdown 檔案裡,再也不用往文件裡複製程式碼了

Literate programming 將 Markdown 檔案作為單一事實來源,使文件、測試和實作保持同步。以下是如何用三十行 Python 實現它。

你的文件、測試和程式碼是三份檔案,講著同一個故事,卻講得都很糟糕。 你在原始碼裡更新了函式簽名,忘了改 README 裡的範例。一週後,新進員工把過時的程式碼片段複製到了生產環境。你的測試檔案仍然把舊的行為編碼為預期結果。現在你有兩個 bug 和一個文件工單。…

你的 Claude 對話已經是文件了。只是它會在 12 小時後消失。

LLM 對話包含意圖、被拒絕的替代方案以及可執行的程式碼。這正是文件應該包含的內容。以下是將 ephemeral chat 轉換為持久、可搜尋的文件,同時不遺失敘事的方法。

你花了 45 分鐘和 Claude 設計一個 retry circuit。你解釋了 failure modes,因為 exponential backoff 會掩蓋 cascading pressure 而拒絕了它,確定了 token-bucket rate limiting with…

文字編輯器讓你寫無效程式碼。樹編輯器不會

每個編譯器都將你的程式碼視為樹,但你的編輯器讓你編輯原始文字。以下是結構化編輯的實際樣子、為什麼它沒有佔領市場,以及如何在不更換工具的情況下借用其優勢。

每種程式語言都有形式語法。編譯器讀取它,構建剖析樹,拒絕任何不符合的內容。編輯器完全無視語法,讓你想輸入什麼就輸入什麼。 這種脫節是大量摩擦的驚人來源。自動完成建議的識別碼在上下文中毫無意義。語法突顯在重構中途崩潰。編輯器眼睜睜看著你犯錯,然後報出「Unexpected…

Donald Knuth希望程式讀起來像文學作品。編譯器另有打算。

Literate programming承諾程式碼應該首先為人類編寫,其次才是為機器。四十年後,幾乎沒有人這樣寫。以下是軟體文件化中最優雅的理念為何未能改變我們工作方式的原因。

1984年,Donald Knuth發表了一篇提出根本性反轉的論文。程式不應該是為編譯器編寫、為人類添加註解的。它們應該被寫作為人類的文學作品,編譯器從中提取可執行部分。他稱之為literate programming,並以此方式建構了TeX。 這個想法很美。它在現代軟體開發中也幾乎完全缺席。…