2009/05/31

迷路

最近 Agda mailing list 上有一串關於 proof irrelevance 的討論。我記得我第一次問「什麼是 proof irrelevance」是跟 scm 老師一塊去 Nottingham 參加 DTP 2008 的時候。後來 XOO 做了一些 survey,聽下來雖然有點零碎的直覺,但總體而言仍然一頭霧水,連大地圖都還畫不出來。例如:Curry-Howard correspondence 和 proof irrelevance 的關係是什麼?(Proof irrelevance 是用來當作 Curry-Howard 的 "patch" 嗎?)引進 proof irrelevance 的目的是什麼?(區分計算上「有趣」和「不有趣」的程式 / 證明?)和一般 intuitionistic logic 相比,我們希望達成的性質有哪些以及為什麼?(Prop 上的排中律?Set/Prop 的分野到底是什麼啊?)不希望破壞的性質有哪些以及為什麼?… 這類的問題我都不清楚答案…

寫總回顧的時候寫到大一時蔡聰明老師囑咐我們要把(微積分)理論的脈絡畫得一清二楚。我沒特別記在心上,但這似乎已經成了我的最高指導原則 ─ 我覺得要做到這樣才算通透。不過除了高等微積分和 Essential OOP(或許還包括正在寫的總回顧)以外,我似乎很少明確做這件事情,頂多在心裡隨便描一下部份流向而已。這或許是大學時代最大的遺憾…

--
這也解釋了為什麼這四年沒有「跑到 100%」的感覺 XD。

Labels:

Anonymous scm6/01/2009 11:00 am 說:

我當時給你的答案大概是「不知道」吧...

Now I still don't know much that you don't.

 
Blogger XOO6/01/2009 4:56 pm 說:

哎,我也不曉得 ...

 
Blogger lotis6/02/2009 6:06 pm 說:

Josh大你好
今年剛讀完大一的資工系學生(不是台大otz
我想請問一下如果要成為一個學術取向的軟工人
有沒有哪些不是資工系內但卻是非常重要得課程要去修呢?
或者是有哪些大作非拜讀不可?
目前我知道大概有c++ primer ,intorduction to Algorithm,essential c++,modern c++ desgin ,code complete , head first desgin pattern ,Numerical.Recipes(←還在考慮要不要看這本)...
可否給個建議
感謝!

 
Blogger Josh Ko6/03/2009 7:02 am 說:

不太清楚你所謂「學術取向的軟工人」確切是指什麼,不過感覺上只要把大學課程紮實修一修應該就有一定程度了,剩下的大概是大型專案的實作經驗吧。Object-oriented XXX 現在還算是顯學,所以可以多看一點。有餘力也可以看看「未來的希望」functional programming XD。

大概幫不到太多忙,因為我(至少暫時)不會和現在所謂的軟工很有關係 :P。

 

<< 回到主頁