文字編輯器讓你寫無效程式碼。樹編輯器不會
每個編譯器都將你的程式碼視為樹，但你的編輯器讓你編輯原始文字。以下是結構化編輯的實際樣子、為什麼它沒有佔領市場，以及如何在不更換工具的情況下借用其優勢。
每種程式語言都有形式語法。編譯器讀取它，構建剖析樹，拒絕任何不符合的內容。編輯器完全無視語法，讓你想輸入什麼就輸入什麼。 這種脫節是大量摩擦的驚人來源。自動完成建議的識別碼在上下文中毫無意義。語法突顯在重構中途崩潰。編輯器眼睜睜看著你犯錯，然後報出「Unexpected…
想法與洞見
探索 AI 優先開發、編碼護欄和可處置架構。
Donald Knuth希望程式讀起來像文學作品。編譯器另有打算。
Literate programming承諾程式碼應該首先為人類編寫，其次才是為機器。四十年後，幾乎沒有人這樣寫。以下是軟體文件化中最優雅的理念為何未能改變我們工作方式的原因。
1984年，Donald Knuth發表了一篇提出根本性反轉的論文。程式不應該是為編譯器編寫、為人類添加註解的。它們應該被寫作為人類的文學作品，編譯器從中提取可執行部分。他稱之為literate programming，並以此方式建構了TeX。 這個想法很美。它在現代軟體開發中也幾乎完全缺席。…
修復缺陷是容易的部分。弄清楚它為什麼存在才是重要的
大多數團隊修復缺陷後就繼續前進。同樣的缺陷反覆出現。以下是如何在費根審查內部執行因果分析，從而停止兩次編寫同樣的缺陷。
每個團隊都有一個反覆出現的缺陷。分頁中的差一錯誤。認證middleware中缺失的空值檢查。三個衝刺前有人「修復過」的結帳race condition。 你並不是三次寫了同一個缺陷。你寫了三個具有相同原因的不同缺陷。修復處理的是症狀。原因依然隱藏。…
Pull Request 審查能發現 15-30% 的缺陷。資料 50 年前就已給出答案。
IBM、AT&T、HP 與 Microsoft 的多項研究均證實，非正式程式碼審查大約能發現四分之一的缺陷。以下是資料實際說明的內容、該比例偏低的原因以及解決方法。
非正式程式碼審查能夠發現被審程式碼中 15% 到 30% 的缺陷。這不是觀點，而是在四十年、多家公司、數十項研究中反覆驗證的結論。 麥可·費根於 1976 年在 IBM 記錄了這一資料。1987 年 AT&T 貝爾實驗室的研究發現了 20%。1996 年惠普的研究發現了 25%。2013…
通用檢查清單什麼都抓不到。結構化檢查清單能發現60%的缺陷。
大多數審查檢查清單都是複製貼上的良好願望列表。Fagan inspection風格的結構化檢查清單基於實際缺陷數據構建，針對特定工件類型，並在個人準備階段使用。以下是如何構建一個有效的檢查清單。
如果你的團隊有一份程式碼審查檢查清單，它很有可能躺在沒人打開的維基頁面上。上面大概寫著「check for off-by-one errors」和「verify error handling」之類的話。這些話都是對的。但也過於籠統，不足以改變行為。 一份告訴你「check for…
大型語言模型可以預先審查你的程式碼，但它無法主持會議
費根審查需要四到六個人、兩小時才能審完250行程式碼。大型語言模型可以透過承擔準備工作與檢查清單的執行來削減這部分成本，但它無法取代人類角色去發現最昂貴的缺陷。
一次完整的費根審查需要一名主持人、一名朗讀員、兩到四名審查員，以及作者本人。團隊以每小時125行的速度，花費兩小時審查大約250行程式碼。這意味著一次小小的改動就要消耗八到十二人時。 大型語言模型可以在不到一秒內讀完250行程式碼。它可以執行檢查清單、標記可疑模式，並在任何人開啟檔案之前就產生一份結構化的缺陷紀錄。…
Fagan Inspections 在測試前發現90%的缺陷。然後我們不再使用它。
Michael Fagan 在 IBM 設計的結構化審查流程，能在程式碼進入編譯器之前捕獲幾乎全部缺陷。但它也消耗了專案總工時的15%–20%。本文解釋軟體史上最有效的審查方法為何消失，以及團隊究竟失去了什麼。
1976年，Michael Fagan 在 IBM Systems Journal 上發表了一篇論文，描述了一種審查流程，其有效性使之成為軟體品質的金標準。Fagan Inspections 在尚未執行任何測試之前，就能捕獲全部缺陷的60%到90%。NASA…
你最優秀的審查員也會遺漏大多數缺陷。Fagan 於1976年在IBM測量了這一點。
即使是高級工程師，在非結構化審查中也只能發現一小部分缺陷。Michael Fagan 在IBM的研究揭示了原因，並建構了結構化審查流程來解決這一問題。
兩位高級工程師審查同一份拉取請求。一位標記了缺失的空值檢查。另一位發現了清理路徑中的競態條件。兩人都沒有發現全部問題。 如果你只指派了一位審查員，那麼其中一個缺陷就會被發布上線。這不是技能差距。這是人類注意力的可預測特性，而 Michael Fagan 於1976年在IBM記錄了這一現象。 Fagan…
大多數程式碼審查只能發現20%的缺陷。Fagan Inspection能發現90%。
非正式的程式碼審查只能發現15%到30%的缺陷。Fagan Inspection是一種有50年歷史的結構化流程，持續報告60%到90%的缺陷移除率。以下是它的運作原理、團隊迴避它的原因，以及如何執行輕量級版本。
大多數程式碼審查只能發現本應找到的缺陷的15%到30%。這不是猜測。IBM在20世紀70年代就測量過，AT&T、惠普和微軟的研究也在數十年間反覆確認了這一範圍。 非正式審查成本低廉、非同步進行、 socially…
AutoVerus將40小時的證明編寫變成3次LLM呼叫。訣竅在於知道何時放棄。
AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。
形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。 給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。…