2008/01/22

熱血點

開始讀 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

Labels:

<< 回到主頁