$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2009/04/21

### Curry-Howard, once again

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 有份投影片

Labels: