一些科學(xué)發(fā)現(xiàn)被賦予了重要的意義，因為揭示了一些新的東西，比如 DNA 的雙螺旋結(jié)構(gòu)或黑洞的存在。但是，揭示出的這些東西還具有更深遠的意義，因為它們表明：兩個之前看起來大不一樣的老舊概念事實上卻是一樣的。比如詹姆斯?克拉克?麥克斯韋發(fā)現(xiàn)的方程組表明，電與磁是同一個現(xiàn)象的兩個不同方面，而廣義相對論則把引力和彎曲的時空聯(lián)系到了一起。

柯里-霍華德對應(yīng)（Curry-Howard correspondence）也是一樣，并且它關(guān)聯(lián)的不僅僅是一個領(lǐng)域中的兩個不同概念，而是兩個完整的學(xué)科：計算機科學(xué)和數(shù)學(xué)邏輯。這種對應(yīng)關(guān)系也被稱為柯里 - 霍華德同構(gòu)（Curry-Howard isomorphism，同構(gòu)是指兩個事物之間存在某種一一對應(yīng)關(guān)系），其為數(shù)學(xué)證明和計算機程序建立了某種關(guān)聯(lián)。

簡單來說，柯里-霍華德對應(yīng)認為：計算機科學(xué)中的兩個概念（類型和程序）分別等價于邏輯學(xué)中的兩個概念（命題和證明）。

這種對應(yīng)關(guān)系導(dǎo)致的一個結(jié)果是程序開發(fā)被提升到了理想化的數(shù)學(xué)層面，而之前人們通常認為程序開發(fā)就是個手藝活。程序開發(fā)不只是「寫代碼」，還變成了證明定理的行為。這能對程序開發(fā)的行為進行形式化，并能提供用數(shù)學(xué)方法推理程序正確性的方法。

而這種對應(yīng)關(guān)系的名稱則來自于兩位研究者，他們各自獨立地發(fā)現(xiàn)了這一對應(yīng)關(guān)系。1934 年，數(shù)學(xué)家和邏輯學(xué)家哈斯凱爾?柯里（Haskell Curry）注意到了數(shù)學(xué)中的函數(shù)和邏輯學(xué)中的蘊涵（implication）關(guān)系之間的相似性。蘊涵關(guān)系的形式是兩個命題之間呈現(xiàn)「if-then（如果 - 那么）」陳述的形式。

受柯里觀察到的結(jié)果的啟發(fā)，數(shù)理邏輯學(xué)家威廉?阿爾文?霍華德 （William Alvin Howard）在 1969 年發(fā)現(xiàn)計算和邏輯之間存在更深度的關(guān)聯(lián)；他的研究表明：運行計算機程序非常像是簡化邏輯證明。在運行計算機程序時，每一行代碼都會被「評估」以產(chǎn)生一個輸出。類似地，在進行一個證明時，一開始是復(fù)雜的陳述，然后對其進行簡化（例如通過消除冗余步驟或用更簡單的表達式替換復(fù)雜表達式），直到得到某個結(jié)論 —— 從許多過渡陳述推導(dǎo)出一個更簡明的陳述。

盡管這一描述大致說明了這種對應(yīng)關(guān)系的含義，但要完全理解它，就需要更多地了解計算機科學(xué)家口中的「類型論（type theory）」。

讓我們從一個著名的悖論談起：在一個村莊中有一位理發(fā)師，他為且只為所有不給自己刮胡子的人刮胡子。那么這位理發(fā)師給自己刮胡子嗎？如果答案為是，那么他就必定不為自己刮胡子（因為他只為不給自己刮胡子的人刮胡子）。如果答案為否，那么他就必定給自己刮胡子（因為他為所有不給自己刮胡子的人刮胡子）。這是伯特蘭?羅素（Bertrand Russell）發(fā)現(xiàn)的一個悖論的非形式化版本，那時候他正嘗試使用名為集合（set）的概念構(gòu)建數(shù)學(xué)的基礎(chǔ)。也即：定義一個包含所有不包含自身的集合的集合是不可能的，這個過程必然會出現(xiàn)矛盾。

羅素的研究表明，為了避免這個悖論，我們可以使用類型（type）。粗略地說，類型是指一些類別，其含有的具體值被稱為對象（object）。舉個例子，如果有一個類型 Nat 表示自然數(shù)，那么其對象就是 1、2、3 等等。研究人員通常使用冒號來表示對象的類型。比如對于整數(shù)類型的數(shù)值 7，可以寫成「7: Integer」。我們可以使用函數(shù)將類型 A 的對象轉(zhuǎn)換成類型 B 的對象，也可以使用函數(shù)將類型 A 和 B 的兩個對象組成一個新類型「A×B」的對象。

因此，為了解決這個悖論，一種方法是對這些類型進行分層，讓它們僅包含比其自身低一個層級的元素。然后一個類型不能包含自身，這就能避免造成上述悖論的自我指涉。

在類型論的世界中，證明一個陳述為真的過程可能與我們習(xí)慣的做法不一樣。如果我們想證明整數(shù) 8 是偶數(shù)，那么問題的關(guān)鍵在于證明 8 實際上是「偶數(shù)」類型中一個對象，而這個類型定義元素的規(guī)則是能被 2 整除。在驗證了 8 能被 2 整除后，我們就能得出結(jié)論：8 就是「偶數(shù)」類型中的一個「居民」。

柯里與霍華德證明類型在根本上等價于邏輯命題。當(dāng)一個函數(shù)「居留（inhabit）」于某一類型時，也就是該函數(shù)是該類型的一個對象時，我們就能有效地證明對應(yīng)的命題為真。因此，以類型 A 的對象為輸入、以類型 B 的為輸出的函數(shù)（表示成類型 A→B）必定對應(yīng)于一個蘊涵：「如果 A，那么 B?！古e個例子，假設(shè)有命題「如果下雨，那么地面是濕的?！乖陬愋驼撝校@個命題會被建模成類型「下雨→地面濕」的一個函數(shù)。這兩種表示方式看起來不一樣，但在數(shù)學(xué)上卻是一樣的。

盡管這種關(guān)聯(lián)看起來可能很抽象，但它不僅改變了數(shù)學(xué)和計算機科學(xué)的實踐者思考其工作的方式，還為這兩個領(lǐng)域帶來了一些實用的應(yīng)用。在計算機科學(xué)領(lǐng)域，這種關(guān)聯(lián)為軟件驗證（即確保軟件正確性的過程）提供了一個理論基礎(chǔ)。通過邏輯命題的方式描述所需行為，程序開發(fā)者可以通過數(shù)學(xué)方式證明一個程序的行為是否符合預(yù)期。并且在設(shè)計更強大的函數(shù)式編程語言方面，這種關(guān)聯(lián)也提供了堅實的理論基礎(chǔ)。

而在數(shù)學(xué)領(lǐng)域，這種對應(yīng)關(guān)系已經(jīng)催生出了證明助手（proof assistant）工具，其也被稱為交互式定理證明器（interactive theorem prover）。這些軟件工具可以輔助構(gòu)建形式化證明，具體的例子包括 Coq 和 Lean。在 Coq 中，每一步證明本質(zhì)上都是一個程序，而證明的有效性則會通過類型檢查算法來檢驗。數(shù)學(xué)家們也已經(jīng)在使用證明助手（尤其是 Lean 定理證明器）來對數(shù)學(xué)進行形式化，其中涉及到以一種可通過計算機驗證的嚴格格式來表示數(shù)學(xué)概念、定理和證明。這讓有時候非形式化的數(shù)學(xué)語言可以通過計算機加以檢驗。

研究者還在探索數(shù)學(xué)和編程之間的這種關(guān)聯(lián)的潛在成果。原始的柯里 - 霍華德對應(yīng)將程序開發(fā)與某種名為直覺邏輯（intuitionistic logic）的邏輯融合到了一起，但事實證明還有更多邏輯類型可以被統(tǒng)一進來。

康奈爾大學(xué)計算機科學(xué)家 Michael Clarkson 說：「自柯里得出其見解的這一個世紀里，我們不斷發(fā)現(xiàn)越來越多『邏輯系統(tǒng) X 對應(yīng)于計算系統(tǒng) Y』的實例?！寡芯空咭惨呀?jīng)將編程和其它類型的邏輯聯(lián)系起來，比如包含「資源」概念的線性邏輯以及涉及可能性和必要性概念的模態(tài)邏輯。

而且盡管這個對應(yīng)關(guān)系秉承柯里與霍華德之名，但他們絕不是這種對應(yīng)關(guān)系的唯二發(fā)現(xiàn)者。這佐證了這種對應(yīng)關(guān)系的一個根本性質(zhì)：人們反復(fù)不斷地一次又一次地注意到它。Clarkson 說：「計算和邏輯之間存在深度關(guān)聯(lián)似乎并非偶然?！?/p>