Hackers

因為跟了隨機客的專題，對於那邊 algorithms research 的情況逐漸有點體驗。其實那邊除了研究對象換成 algorithms 以外，做的事情和一般數學家沒什麼差別。特別地（in particular），他們對於演算法的描述並不講究，證明內容豐富但型式天馬行空，就好像我們現在看 60, 70 年代的 hackers 寫程式一樣（Curry-Howard, informally XD），有天才的成就，但寫出的程式（包括證明）沒什麼結構。看他們在證明就好像在鋼索上跳舞一樣，看得下面的人心驚膽跳。可是這邊「怎麼寫好程式和證明」的理論還遠遠追不上他們，只好先讓他們繼續跳了 XD。

還有一個現象是，他們（和數學家）所謂的 constructive proofs 是存在演算法能構造出 desired objects，但證明演算法正確性時大量使用反證法。所以 existential proposition 的 witness 確實找到了，但「這個 witness 符合規格」的證明只在 classical logic 下面有效。其實我不太了解這樣到底發生什麼事…

另一方面，「假裝自己其實看得懂」地硬鑽 HOAS paper 似乎有點成果。看著 Yoneda lemma 把「表示成某種 functors 的 meta-level terms」和「表示成某種 arrows 的 object-level terms」拉在一起還挺炫的 XD。

--
選定領域後帶著立場看看其他領域，收穫反而更大 XD。