迷路

最近 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。