型式化革命

前一陣子覺得 formalisation 很難推銷給一般做理論的人，認為大概要有某種知識論上的偏執才會嚴肅看待 formalisation。可是這幾天看演算法與證明看得幾乎要吐血 ─ 不利閱讀是通病就算了，內容鬆散到根本不知道演算法是怎麼算的。現在我覺得型式化革命 ─ 讓寫證明的人都寫（或至少練習過）型式化證明 ─ 是相當必要的了 XD。

今日飲食：晚上帶筋牛肉麵 + 燙青菜 @ 台大牛肉麵（$160）+ 蘋果汁 @ 男七販賣機（$13）。合計 $173。

--
Lamport 試著革命過但失敗了，真可惜 XD。

---

譯兩段 Lamport 的批評出來：

現用的數學符號已然經過幾百年的演化，但證明風格卻還停滯在十七世紀。數學家比較保守一些，很多人不願意考慮寫證明有沒有更好的方式。但是有人告訴我，數學家知道他們發表錯誤定理時會覺得很羞愧，所以他們有避免錯誤的動力。我相信如果有人說服他們試寫結構化證明，他們會喜歡的。

計算機科學家比較願意探索非制式的證明風格。但很不幸的是，我發現很少有人理會他們發表的結果是不是錯的。當覆審者沒發現錯誤時，他們往往感到很安慰 ─ 被發現的話可就少了一篇論文。我擔心沒多少計算機科學家會有動機採用使錯誤更容易現形的證明風格。除非錯誤結果不再被視為正常現象而是令人尷尬的情況，計算機科學界不太可能廣泛採用結構化證明。

--
實在嗆得令人爽快 XD。