一龍馬/AI 情報站讀懂消息背後的脈絡
星期三
搜尋

Galois 的 Mike Dodds 主張,形式驗證的主要瓶頸常不是證明技術,而是系統根本缺乏精確、一致且可長期維持的形式規格

中文摘要

編譯器、密碼函式庫、剖析器與微核心具有清楚邊界和較穩定的數學描述,因此驗證雖昂貴但可行;瀏覽器、文書軟體甚至 PDF 等龐雜系統,則未必存在各方都同意的完整規格。HN 回應提出中間地帶,例如銀行 App 可把部分 UI 行為描述成狀態機,但介面頻繁改版及規格如何連回程式碼仍是難題。

一龍馬判讀

這把形式方法專案的風險往前推到「到底要保證什麼」:企業若未先界定穩定邊界與可驗證性質,再多證明資源也可能只驗證了錯誤或迅速過時的目標。LLM 從實作反推規格或許能降低成本,但目前討論只提出方向,沒有足夠證據證明它能解決規格本身的歧義。

原文節錄

Hacker News · surprisetalk

Galois - Specifications Don't Exist Our Work Research Advanced Cryptography & Privacy AI / ML and Data Science Rigorous Digital Engineering Software & Systems A

取得部分原文 · 不代表內容已獨立查證

查看原文 閱讀社群討論
完整收錄文字與來源

Specifications Don't Exist (2025)

收錄日期
2026-09-02
來源
Hacker News Firebase API
抓取時間
2026/09/02 05:40(台北)
來源資料
29 分 · 2 則討論