探索 AI 優先開發、編碼護欄和可處置架構。
Cleanroom 驗證需要生成並消除證明義務（proof obligations）。以下說明 LLM 如何自動化註解與驗證條件（VC）的生成，讓你能專注於真正困難的證明工作。
Cleanroom 軟體工程要求你在編譯程式碼之前，先證明它是正確的。這聽起來很高尚，直到你花了三個小時為一個只排序十個整數的函式撰寫迴圈不變式（loop invariant）為止。 瓶頸不在證明本身，而在於那些繁瑣的樣板程式碼。生成驗證條件（verification…
Cleanroom software engineering 將 defect rate 降低 100 倍，但全面採用需要獨立的 test team 和 formal proof。這裡介紹一種 pragmatic subset，無需 overhead 即可捕獲大部分收益。
Cleanroom software engineering 每千行程式碼僅產生 0.1 個缺陷。業界平均水準是 10 到 50。問題是，完整的 Cleanroom 要求你將團隊拆分為 author 和 verifier，在每個 module 之前編寫 formal specification，並禁止…
IBM 的 Cleanroom engineering 達到了比業界平均水準好 100 倍的 defect rate，然後消失在歷史中。它的消失與是否有效毫無關係。
IBM 的 Cleanroom software engineering process 實現了每千行程式碼 0.1 個 defect。當時的業界平均水準在 10 到 50 之間。該 process 被文件化，在多個專案和語言之間 replicate，並經過獨立驗證。然後它消失了。 不是因為更好的 method…
Cleanroom software engineering 承諾透過 mathematical verification 而非 debugging 實現零缺陷增量。我們查看 IBM 的實際專案資料，看看這一說法是否成立。
1980 年代軟體業的平均水平是每千行程式碼 30 到 60 個缺陷。IBM 的 Cleanroom 團隊交付了一個 2 萬行的編譯器增量，在測試中發現了 53 個缺陷。也就是每 KLOC 2.6 個。一些 1 萬行的獨立增量在進入系統測試時，沒有發現任何缺陷。 最離奇的部分？程式設計師被禁止執行自己的程式碼。…
Box Structure 強制你將模組的行為、記憶的狀態和實作方式定義為三個獨立且可驗證的層。以下是 Cleanroom 如何利用它們消除除錯。
你先寫程式碼，再寫測試，然後發現程式碼是錯的。這是標準循環。也是為什麼除錯會消耗大多數專案時間線的一半。 Box Structure 把這個過程反轉。你在寫程式碼之前就定義行為，用數學方式驗證這個定義，然後一層一層翻譯成程式碼。結果是「構造即正確」的模組，而不是「測試碰巧通過所以正確」。…
IBM 的 Cleanroom 工程流程透過預防而非發現缺陷，達成了比業界平均好 100 倍的缺陷率。以下是它的運作方式、為何幾乎無人使用，以及你今天可以借鏡什麼。
IBM 交付了一套 NASA 衛星控制系統，每千行程式碼僅有 0.1 個缺陷。當時的業界平均水準在 10 到 50 之間。他們並非依靠招聘更聰明的工程師或延長工作時間來達成這項目標。他們靠的是禁止開發者執行自己的程式碼。 這就是 Cleanroom 軟體工程，由 IBM 的 Harlan Mills 於 1970…
Literate programming 承諾單一事實來源，但手動的 weave 和 tangle 步驟會破壞 CI/CD 流水線。以下是如何自動化提取和文件生成，使 Markdown 檔案保持規範。
如果你的建置流水線必須等你開啟終端機輸入 才能執行，那你就沒有文學化程式。你有的只是一本綁著編譯器的日記。 文學化程式設計的全部意義在於散文和程式碼共享單一事實來源。Markdown 檔案就是產物。其他一切——可執行原始碼、渲染後的文件、測試檔案——都是衍生的。衍生產物屬於 CI，不屬於你的工作記憶。 問題不是 CI…
我花了30天時間，在向LLM索取程式碼之前先撰寫設計說明。結果改變了我對rubber-ducking的看法。
大多數開發者把LLM用反了。我們用五個詞描述需求，拿回200行程式碼，然後花下一個小時除錯模型做出的假設。 我花了三個月時間執行相反的流程：在索取哪怕一行程式碼之前，先寫一份完整的設計說明。結果程式碼缺陷更少了，但真正的進步在於我自己的理解。 Donald Knuth在1984年提出了「literate…
Literate programming 將 Markdown 檔案作為單一事實來源，使文件、測試和實作保持同步。以下是如何用三十行 Python 實現它。
你的文件、測試和程式碼是三份檔案，講著同一個故事，卻講得都很糟糕。 你在原始碼裡更新了函式簽名，忘了改 README 裡的範例。一週後，新進員工把過時的程式碼片段複製到了生產環境。你的測試檔案仍然把舊的行為編碼為預期結果。現在你有兩個 bug 和一個文件工單。…
LLM 對話包含意圖、被拒絕的替代方案以及可執行的程式碼。這正是文件應該包含的內容。以下是將 ephemeral chat 轉換為持久、可搜尋的文件，同時不遺失敘事的方法。
你花了 45 分鐘和 Claude 設計一個 retry circuit。你解釋了 failure modes，因為 exponential backoff 會掩蓋 cascading pressure 而拒絕了它，確定了 token-bucket rate limiting with…