2008/01/05

雜記

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。

Labels:

Anonymous scm1/06/2008 7:04 am 說:

>其實一般程式員迫切需要的不是完整的正確性證明...程式語言設計者只要提供很簡單的機制

Indeed! On the other hand, the I/O relation is also merely one aspect of "correctness". It does not cover things like efficiency, deadlock-free, etc.

When it comes to correctness we are always doing an approximation. Sometimes a simple approximation (array bound checking, etc) would be sufficient. In the next phase of our research, I would like to look at these aspects too.

Heading to PEPM... see you guys 2 weeks later.

 

<< 回到主頁