雜記

FLOLAC 的眾位老師在討論每週大家一起來 meeting，地點可能在台大資管系。想想其實還滿恐怖的，例如蔡老師說不定就把全部的研究生帶過來，像 FLOLAC 那樣滿場都是自己人（有一半吧？XD），然後每個星期就聽 program verification 就好了 XD。然後地點改在台大資管系好像就少了長途跋涉的樂趣（？），沒有遠足的感覺 XD。（坐交通車和坐遊覽車感覺很像 XD。）

關於 Tim Sweeney 演講的一點感想：scm 老師在 paper 裡面寫「用來介紹 dependently typed programming 的例子常常只是證明一些很簡單的性質，像是串接或反轉 lists 之後長度和原本的 lists 有某些關連…」（這我大致意譯的 XD），但是看完 Sweeney 投影片的一些統計，其實一般程式員迫切需要的不是完整的正確性證明（光一個 insertion sort 就滿難證了 XD），程式語言設計者只要提供很簡單的機制確保像 out-of-bounds array access、null pointer dereference 這種錯誤不會出現在編譯成功的程式裡面，就可以砍殺 50% 的 bugs！感覺又是一條 80-20 法則 ─ 用 20% 的理論解決 80% 的實務問題。

--
意見可能很 trivial 啦，可是有寫下來總比沒寫好 XD。