Curry-Howard, once again

看到 Alex Laburu 聽 Lamport 講 How to Write a Proof 的筆記，其中一段又明顯地勾起 Curry-Howard。以下藍色的字是我加的：

Most mathematicians (programmers) wish to make proofs (programs) easier to write, but Dr. Lamport wants to make proofs (programs) harder to write — but only because this is what it will take, he claims, to make proofs (programs) easier to read. The primary motivation for such an undertaking is that approximately one-third (some ratio here) of all published proofs (released software) have serious errors (bugs), even after peer-review (testing); therefore, making proofs (programs) easier to read should take precedence over making proofs (programs) easier to write.

「讓程式變難寫也更難錯」正是 scm 老師常用來廣告 dependently-typed programming 的詞！唯一偏離的大概是 dependently-typed programs 沒比較好讀吧… 不過對於 type checker 而言或許比較「好讀」沒錯 XD。

--
Lamport 有份投影片。