🌕 命題即類型
➤ 邏輯與計算的深層連結
✤ https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
本文探討了「命題即類型」原理，闡述了邏輯學與計算機科學之間深刻的關聯。這個原理認為，邏輯中的命題與程式語言中的類型相互對應，命題的證明則對應於程式，簡而言之，命題即類型，證明即程式。該原理源於20世紀30年代的直覺主義邏輯研究，並由多位科學家獨立發展，影響深遠，催生了自動證明輔助工具和多種程式語言。文章追溯了其歷史源流，並探討了其背後深層的哲學和數學意義。
+ 這篇文章讓我意識到數學、邏輯和程式設計之間存在著更深層次的聯繫，以前從未這樣想過！
+ 我對這個原理的歷史發展過程感到非常驚訝，原來這麼多科學家都參與其中，真是令人著迷。
#計算機科學 #邏輯學 #程式語言