透過 lcamel 的介紹得知了「數學：確定性失落」(Mathematics: The loss of Certainty) 這本書。 作者 Morris Kline 有感於現今數學學院越來越走向純數研究，漸漸地遺忘數學乃科學之母，而寫的一本回顧數學歷史的書。 歷史上數學在許多關鍵時刻扮演了提供科學前進方向的指引。從科學研究提供出來的數據，發明新的數學工具，整理出一套觀點。 我們所熟知的大數學家在那個年代也往往是物理學家，天文學家。並且從不以數學家自稱。 他希望藉由歷史上眾多的經驗，來論述自己認為應該回到以往科學與數學間角色的立場。 而非讓純數派的數學家輕視被歸類為應用數學派的數學家。 至於本文為什麼要將數學史與程式語言理論放在一起呢？ 因為程式語言理論恰恰是近代數學危機之後，從理論發展的工具所衍生出來的。 而這本書對於數學近代史有著非常完整的介紹， 陳述了「邏輯主義」、「直覺主義」、「形式主義」與「集合論派」等等的觀點。 並說明了哥爾德不完備定理與之後的洛溫罕斯寇楞理論而導致數學基礎上的分歧（或是悲觀一點也可以看作毀滅）。 現代大學數學系所教的數學主流，多半還是集合論 ZF 公設出發來推導的一整個架構，但那也僅僅只是一種觀點而已。 這些歷史沒有跟程式語言理論的數學直接相關， 但就跟去思考為什麼有人發明微積分，整個歷史演進、整個大環境與他的思路究竟是怎麼導致這項發明的一樣。 天才雖是天才，但受限於時代，畢竟還是要有所本才能得出這些發現或發明。 由於程式語言理論奠基於數理邏輯與形式系統的發展上， 恰恰好就是這個時代試圖為數學奠定基礎的發明。 熟悉這些歷史能夠讓我們稍微窺探到這些天才們的狐狸尾巴。
在這段歷史中，對於計算科學界最重要的就是為了解決 Hilbert 所謂的 Entscheidungsproblem (Decision Problem) 而獨立分別發明的 Turing Machine 與 Lambda Calculus。 雖然 Hilbert 的原意並不是為了計算理論，而是為了數學的基礎打底。 他在 1928 年的 conference 提出他的問題 “First, was mathematics complete… Second, was mathematics consistent… And thirdly, was mathematics decidable?” 所謂的 decidable 就是說，給任何一個清楚描述的數學陳述，由於在古典邏輯裡面，我們承認了排中律。 也就是一個陳述要碼為真，否則就是否。 既然我們這樣先驗了排中律，那剩下的問題就是我們是否能夠從既有承認的陳述，經過有限次的推導，來決定給定的數學陳述究竟是真還是假。 是否有這樣一個一般性適用的 algorithm 存在。 而 Alan Turing 與 Alonzo Church 都給出了否定的答案。 Turing Machine 與 Lambda Calculus 就是他們為了證明而構造的形式系統（要定義何謂 algorithm，就必須先給出形式系統）。 當初並非想拿來套用成計算理論，而是邏輯方面的應用。 後來 Church 也有意識到 Lambda Calculus 可以作為運算模型的潛力，並證明了他跟 Turing Machine 等價。 並為了在邏輯上避開羅素悖論，又多改進了第一版的 Lambda Calculus，加上型態變成 Simply Typed Lambda Calculus。 同樣地 Church 的這一項創作，又被應用至非他本意的領域，也就是後來的程式語言理論的型別研究部分。
退一萬步來看，所謂的 Programming 就是在給定好的形式系統上，構造出你所想要的陳述。 這陳述可能比較簡單如 x + y 的結果，複雜可能是一個 web server。 這時候很自然的一個問題就是：「你怎麼保證你的構造是對的？」，也就是你宣稱的跟你構造的結果必須是一樣。 如今在我們剛學習程式的時候，這種保證多半是經由我們的直覺推理與測試。 但由於受到 Simply Typed Lambda Calculus 的啟發，理論學家們發現到這種保證是可以藉由型別來自動化做到的。 Simply Typed Lambda Calculus 給我們的啟示就是 Lambda Calculus 用代換形式當作一步演算跟型別的推導是有對應的。 當我們在進行每一步的時候，型別上的推導簡直就跟根琴所提出的 Natural Deduction 的步驟一樣。 而後來根據進一步正式證明而成為 Curry-Howard Correspondence。 這樣我們就知道，型別如 a -> b，其實就是邏輯上的宣稱，你用邏輯的方式陳述你的規格。或是數學的術語就是「定理」 而對應的 Lambda Calculus 的演算，就是我們在對定理的證明。 證明的每一步驟剛好都是針對 Lambda Calculus 這個形式系統，用代換的方式來進行。 因此，Compiler 可以從你的演算來檢查跟你的宣稱是否有不一致的地方。 你是否宣稱一個函數應該輸入整數並輸出整數，最後卻輸出了字串。 這時候機器就能提醒你，你的構造跟你的宣稱不一致，非常有可能是你哪裡搞錯了。
由於 Lambda Calculus 剛好是以 mathematical function 來當作操作單位的形式系統， 所以認知上，好像型別嚴格檢查的語言就是 functional programming 的形式。 但實際上 functional programming 並不一定要伴隨著嚴格的型別。 只是當你哲學上追求「可證明正確」的程式時，我們數學提供的工具，就是從 Church 的 Lambda Calculus 演進而來。 未來也不知道是否會有其他種理論。但現況是如此。 這也是程式語言理論界的主流。
個人覺得程式語言研究好玩的地方在於，充分體現了形式系統多元化的需求，甚至加進實作的考量還會有社會學的因素進來。 學界主流語言追求正確與結構的表達力提供非常好的指引。 但對於現今主流程式語言從草根發展的背景卻不太相搭， 因此儘管許多理論在 1980 年代學界就已經達成共識，在實務上經過了三十年還是無法融入主流。 這當中有許多有趣的因素值得探討。 多少也造就了專家用的形式系統與草根用的形式系統有十分大的差距的現況。 針對任務的出錯成本與轉換成本、資源成本等，也形成了越來越分歧的情形。 資訊科學的蓬勃發展算一算還沒一百年。一百年後的系統，不知道會是什麼樣子。光發想這件事就有讓人細細琢磨的樂趣。