요는 Curry-Howard isomorphism 이란 1st order logic 의 logical fomular 와 simply typed lambda-calculus 의 타입 사이의 isomorphism 입니다. 또한 logic 의 deduction 이 lambda term 과 1-1 correspondence 를 가지게 됩니다. 이는 결국 '증명 가능한 명제' 와 '계산 가능한 함수' 라는 것이 symmetry 를 가진다는 것을 의미합니다.