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

柯里 - 霍華德對應（Curry-Howard correspondence）也是一樣，并且它關聯的不僅僅是一個領域中的兩個不同概念，而是兩個完整的學科：計算機科學和數學邏輯。這種對應關系也被稱為柯里 - 霍華德同構（Curry-Howard isomorphism，同構是指兩個事物之間存在某種一一對應關系），其為數學證明和計算機程序建立了某種關聯。

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

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

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

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

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

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

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

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

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

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

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

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

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

康奈爾大學計算機科學家 Michael Clarkson 說：「自柯里得出其見解的這一個世紀里，我們不斷發現越來越多『邏輯系統 X 對應于計算系統 Y』的實例?！寡芯空咭惨呀泴⒕幊毯推渌愋偷倪壿嬄撓灯饋?，比如包含「資源」概念的線性邏輯以及涉及可能性和必要性概念的模態邏輯。

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