熱血點

開始讀 Tony Hoare 的《Essays in Computing Science》第一篇〈The emperor's old clothes〉，這是 1980 年的 ACM Turing award lecture。Hoare 要選擇 ALGOL 60 的某個子集出來實作時，提出四個原則。其中第一個原則是 security，Hoare 說這個原則的一個推論是在執行期檢查所有 subscripts，例如 array indexes。這讓我很自然地想到 Sweeney 也提過 out-of-bounds array access 是一個主要問題。過了二十年問題都還在，Hoare 大概氣得跳腳 XD。然後我就想到，如果編譯器的 final project 可以自選主題，我就可以來設計一個 "Dependent C"，把一些簡單的 dependent types 移植進去，這樣應該能重拾 TOY86 的熱血感。如果設計的是 "Dependent C++"，恐怕就比 TOY86 更熱血了 XD。可是總覺得這個老師不太可能讓我們自由選題…

例如 array bounds checking，我們可以提供兩種選項。一種是 "self-justificatory"，即執行期檢查 subscripts 是不是落在允許範圍內，和 Java 一樣，這種大概沒什麼好做。另一種選擇是讓程式員提供 static proof（可能會長得很像 Hoare logic），在編譯期就確定不會越界，如此編譯器就能抹掉執行期的檢查。然後可以繼續延伸，例如設計機制讓程式員能自己定義 propositions，讓 return type 可以相依於 argument values 等等。不過馬上想到的一個難處就是 pointers，aliasing 進來會讓事情變得很複雜，所以光做 array bounds checking 可能就有些挑戰。

可是要是 final project 不能自選題目，以上就都是空話。暑假還有更重要的事情要做，不可能停下來做這個東西。

--
可以讓 cyy 教編譯器嗎？XD