當我高中畢業進入大學計算機系的時候，輔導員對我們說：“你們不要只學書本知識，也要多見識一下業界的動態，比如去電腦城看看人家怎么裝機。”當然他說我們要多動手，多長見識，這是對的。不過如果成天就研究怎么“裝機”，研究哪種主板配哪種 CPU 之類的東西，你恐怕以后就只有去電腦城賣電腦了。

本科的時候，我經常發現一些同學不來上數學課。后來卻發現他們在宿舍自己寫程序，對MFC之類的東西津津樂道，引以為豪。當然會用MFC沒有什么不好，可是如果你完全沉迷于這些東西，恐怕就完全局限于Windows的一些表面現象了。

所以我在大學的時候就開始折騰Linux，因為它貌似讓我能夠“深入”到計算機內部。那個時候，書店里只有一本 Linux 的書，封面非常簡陋。這是一本非常古老的書，它教的是怎樣得到Slackware Linux，然后把它從二三十張軟盤裝到電腦上。總之，我就是這樣開始使用Linux的。后來我就走火入魔了，有時候上課居然在看GCC的內部結構文檔。后來我又開始折騰TeX，把TeXbook都看了兩遍，恁是用它寫了我的本科畢業論文。

后來進了清華，因為不滿意有人嘲笑我用Linux這種“像DOS的東西”，以及國內網站都對Windows和IE進行“優化”的情況，就寫了個“完全用Linux工作”。確實，會Linux的人現在更容易找到工作，更容易被人當成高手。但是那些工具同樣的奴役了我，經常以一些雕蟲小技而自豪，讓我看不到如何才能設計出新的，更好的東西。當它們的設計改變的時候，我就會像奴隸一樣被牽著鼻子走。

這也許就是為什么我在清華的圖書館發現《SICP》的時候如此的欣喜。那本書是嶄新的，后面的借書記錄幾乎是空白的。這些看似簡單的東西教會我的，卻比那些大部頭和各種 HOWTO 教會我的更多，因為它們教會我的是WHY，而不只是HOW。當時我就發現，雖然自認為是一個“資深”的研究生，學過那么多種程序語言，各種系統工具甚至內核實現，可是相對于SICP的認識深度，我其實幾乎完全不會寫程序！在第三章，SICP 教會了我如何實現一個面向對象系統。這是我第一次感覺到自己真正的在開始認識和控制自己所用的工具。

因為通常人們認為Scheme不是一個“實用”的語言，沒有很多“庫”可以用，效率也不高，而Common Lisp是“工業標準”，再加上Paul Graham文章的慫恿，所以我就開始了解Common Lisp。在那段時間，我看了Paul Graham的《On Lisp》和Peter Norvig的 《Paradigms of Artificial Intelligence Programming》。怎么說呢？當時我以為自己學到很多，可是現在看來，它們教會我的并沒有《SICP》的東西那么精髓和深刻。開頭以為一山還有一山高，最后回頭望去，其實復雜的東西并不比簡單的好。現在當我再看Paul Graham和Peter Norvig的文章，就覺得相當幼稚了，而且有很大的宗教成分。

進入Cornell之后，因為Cornell的程序語言課是用SML的，我才真正的開始學習“靜態類型”的函數式語言。之前在清華的時候，有個同學建議我試試ML和Haskell，可是因為我對Lisp 的執著，把他的話當成了耳邊風。當然現在用上SML就免不了發現ML的類型系統的一些撓人的問題，所以我就開始了解Haskell，并且由于它看似優美的設計，我把“終極語言”的希望寄托于它。我開始著迷一些像monads，type class，lazy evaluation 一類的東西，看Simon Peyton Jones的一些關于函數式語言編譯器的書。以至于走火入魔，對其它一切“常規”語言都持鄙視態度，看到什么都說“那只不過是個monad”。雖然有些語言被鄙視是合理的，有些卻是被錯怪了的。后來我也發現monad, type class, lazy evaluation這些東西其實并不是什么包治百病的靈丹妙藥。

但是我很不喜歡Cornell的壓抑氣氛，所以最后決定離開。在不知何去何從的時候，我發了一封email給曾經給過我fellowship的IU教授Doug Hofstadter（《GEB》的作者）。我說我不知道該怎么辦，后悔來了 Cornell，我現在對函數式語言感興趣。他跟我說，IU的Dan Friedman就是做函數式語言的啊，你跟他聯系一下，就說是我介紹你來的。我開頭看過一點The Little Schemer，跟小人書似的，所以還以為Friedman是個年輕小伙。當我聯系上Friedman的時候，他貌似早就認識我了一樣。他說當年你的申請材料非常impressive，可惜你最后沒有選擇我們。你要知道，世界上最重要的不是名氣，而是找到賞識你，能夠跟你融洽共事的人。你的材料都還在，我會請委員會重新考慮你的申請。IU 的名氣實在不大，而Friedman 實在是太謙虛了，所以連跟他打電話都沒有明確表態想來IU，只是說“我考慮一下……”這就是我怎么進入IU的。

Friedman的教學真的有一手。雖然每個人對他看法不同，但是有幾個最重要的地方他的指點是幫了我大忙的。有人可能想象不到，在Scheme這種動態類型語言的“老槽”，其實有人對“靜態類型系統”的理解如此深刻。也就是在Friedman的指點下，我發現類型推導系統不過是一種“抽象解釋”，而各種所謂的“typing rule”，不過是抽象解釋器里面的分支語句。我后來就通過這個“直覺”，再加上Friedman的邏輯語言miniKanren里面對邏輯變量和unification的實現，做出了一個Hindley-Milner類型推導系統（HM 系統），也就是ML和 Haskell的類型系統。雖然我在Cornell的課程作業里實現過一個HM系統，但是直到Friedman的提點，我才明白了它“為什么”是那個樣子，以至于達到更加優美的實現。后來經他一句話點撥，我又寫出了一個lazy evaluation的解釋器（也就是Haskell的語義），才發現原來SPJ的書里所謂的“graph reduction”，不過就是如此簡單的思想。只不過在SPJ的書里，細節掩蓋了本質。后來我在之前的HM系統之上做了一個非常小的改動，就實現了type class的功能，并且比Haskell的實現更加靈活。所以，就此我基本上掌握了ML和Haskell的理論精髓。

可是類型系統卻貌似一個無止境的東西。在ML的系統之上，還有System F，Fw，MLF，Martin Lof Type Theory，CIC，……怎么沒完沒了？我一直覺得這些東西過度復雜，有那個必要嗎？直到Amal Ahmed來到IU，我才相信了自己的感覺。然而，這卻是以一種“反面”的方式達到的。

Amal是著名的Andrew Appel（“虎書”的作者）的學生，在類型系統和編譯器的邏輯驗證方面做過很多工作。可是她比較讓人受不了，她總是顯得好像自己是這里唯一懂得類型的人，而其他人都是類型白癡。她不時的提到跟Bob Harper, Benjamin Pierce等類型大牛一起合作的事情。如果你問她什么問題，她經常會回答你：“Bob Harper說……”她提到一個術語的時候總是把它說得無比神奇，把它的提出者的名字叫得異常響亮。有一次她上課給我們講System F，我問她，為什么這個系統有兩個“binder”，貌似太復雜了，為什么不能只用一個？她沒有正面回答，而是嘲諷似的說：“不是你說可以就可以的。它就是這個樣子的。”后來我卻發現其實有另外一個系統，它只有一個binder，而且設計得更加簡潔。后來我又在課程的 ailing list 了一個問題，質疑一個編譯器驗證方面的概念。本來是純粹的學術討論，卻發現這封email根本沒有發到全班同學信箱里，被Amal給moderate掉了！

看到這種種詭異的行為，我才意識到原來學術界存在各種“幫派”。即使一些人的理論完全被更簡單的理論超越，他們也會為“自己人”的理論說話，讓你搞不清到底什么好，什么不好。所以后來我對一些類型系統，以及Hoare Logic一類的“程序邏輯”產生了懷疑。我的課程project報告，就是指出Hoare Logic和Separation Logic所能完成的功能，其實用“符號執行”或者“model checking”就能完成。而這些程序邏輯所做的事情，不過是把程序翻譯成了等價的邏輯表達式而已。到時候你要得知這些邏輯表達式的真偽，又必須經過一個類似程序分析的過程，所以這些邏輯只不過讓你白走了一些彎路。當Amal聽完我的報告，勉強的笑著說：“你告訴了我們這個結論，可是你能用它來做什么呢？”我才發現原來透徹的看法，并不一定能帶來認同。人們都太喜歡“發明”東西，卻不喜歡“歸并”和“簡化”東西。

可是這類型系統的迷霧卻始終沒有散去，像一座大山壓在我頭上。我不滿意Haskell和ML的類型系統，又覺得System F等過于復雜。可是由于它們的“理論性”和它們創造者的“權威”，我不敢斷定自己的看法就不是偏頗的。對付疑惑和恐懼的辦法就是面對它們，看透它們，消滅它們。于是，我利用一個independent study的時間，獨立實現了一個類型系統。我試圖讓它極度的簡單，卻又“包羅萬象”。經過一番努力，這個類型系統“涵蓋”了System F, MLF 以及另外一些類似系統的推導功能，卻不直接“實現”他們。后來我就開始試圖讓它涵蓋一種非常強大的類型系統，叫做intersection types。這種類型系統的研究已經進行了20多年，它不需要程序員寫任何類型標記，卻可以給任何“停機”的程序以類型。著名的Benjamin Pierce當年的博士論文，就是有關intersection types的。沒幾天，我就對自己的系統稍作改動，讓它涵蓋了一種最強大的intersection type系統（System I）的所有功能。然而我卻很快發現這個系統是不能實用的，因為它在進行類型推導的時候相當于是在運行這個程序，這樣類型推導的計算復雜度就會跟這個程序一樣。這肯定是完全不能接受的。后來我才發現，原來已經有人指出了 System I 的這個問題。但是由于我事先實現了這個系統，所以我直接的看到了這個結論，而不需要通過繁瑣的證明。

所以，我對類型推導的探索就這樣到達了一個終點。我的類型系統是如此的簡單，以至于我看到了類型推導的本質，而不需要記住復雜的符號和推理規則。我的系統在去掉了intersection type之后，仍然比System F和MLF都要強大。我也看到了Hindley-Milner系統里面的一個嚴重問題，它導致了這幾十年來很多對于相關類型系統的研究，其實是在解決一個根本不存在的問題。而自動定理證明的研究者們，卻直接的“繞過”了這個問題。這也就是我為什么開始對自動定理證明開始感興趣。

后來對自動定理證明，Partial Evaluation 和 supercompilation的探索，讓我看到那些看似高深的Martin Lof Type Theory, Linear Logic等概念，其實不過也就是用不同的說法來重復相同的話題。具體的內容我現在還不想談，但是我清楚的看到在“形式化”的美麗外衣下，其實有很多等價的，重復的，無聊的東西。與其繼續“鉆研”它們，反復的叨咕差不多的內容，還不如用它們的“精髓”來做點有用的事情。

所以到現在，我已經基本上擺脫了幾乎所有程序語言，編譯器，類型系統，操作系統，邏輯推理系統給我設置的思維障礙。它們對我來說不再是什么神物，它們的設計者對我來說也不再是高不可攀的權威。我很開心，經過這段漫長的探索，讓我自己的思想得到了解放，翻身成為了這些工具的主人。雖然我看到某些理論工具的研究恐怕早就已經到達路的盡頭，然而它們里面隱含的美卻是無價和永恒的。這種美讓我對這個世界的許多其它方面有了煥然一新的看法。一個工具的價值不在于它自己，而在于你如何利用它創造出對人有益的東西，以及如何讓更多的人掌握它。這就是我打算現在去做的。