많은 프로그래머에게 정밀한 수학적 논리 (Mathematical Logic)와 일반적인 프로그래밍은 서로 다른 세계처럼 느껴집니다. 논리는 정리를 증명하는 것에 관한 것이고, 프로그래밍은 시스템이 올바르게 동작하도록 만드는 것에 관한 것입니다. 증명은 수학자의 영역이고, 함수는 엔지니어의 영역입니다. 하지만 Lean과 같은 시스템에서는 이러한 경계가 무너지기 시작합니다. 이 이면에 있는 가장 깊은 아이디어 중 하나는 커리-하워드 대응 관계 (Curry–Howard correspondence)입니다. 즉, 다음과 같은 관찰입니다:

• 논리적 명제 (Logical propositions)는 타입 (Types)에 대응한다.
• 증명 (Proofs)은 프로그램 (Programs)에 대응한다.
• 증명 검사 (Proof checking)는 타입 검사 (Type checking)에 대응한다.

처음에는 이것이 추상적이고 철학적이거나, 심지어 범주론 (Category theory)의 신비주의처럼 들릴 수 있습니다. 하지만 Lean에서 이것이 구체적으로 표현되는 것을 한 번 보고 나면, 매우 기계적인 과정이 됩니다. 이 글은 논리에서 함수로, 증명 목표 (Proof goals)에서 사양을 담은 타입으로, 그리고 문자 그대로 자신의 정당성 증명을 포함하는 정렬 함수로 이어지는 그 전환 과정을 단계별로 살펴봅니다.

핵심 아이디어: 명제는 타입처럼 동작한다
아주 작은 논리적 문장부터 시작해 봅시다: P ∧ Q → P
논리적으로 읽으면 이는 다음과 같습니다: “P와 Q가 모두 참이라면, P는 참이다.” 매우 당연한 이야기입니다. 이제 이를 계산적으로 재해석해 봅시다.

논리적 해석 (Logical Interpretation)
증명하기 위해: P ∧ Q
당신은 다음을 제공해야 합니다:
P의 증명과 Q의 증명
이 구조는 쌍 (Pair): (p, q)와 동일합니다.
마찬가지로, 증명하기 위해: P → Q
당신은 다음을 제공해야 합니다:
P의 증거를 Q의 증거로 변환하는 방법
이것이 바로 함수 (Function)가 하는 일입니다.

따라서 커리-하워드 (Curry–Howard) 하에서는 다음과 같습니다:

이것은 Lean에서 은유가 아닙니다. 문자 그대로의 사실입니다.

작은 정리 또한 하나의 프로그램이다
다음은 Lean의 정리입니다:

theorem fst : P ∧ Q → P := by intro h exact h.left

천천히 읽어봅시다.
목표 (The Goal)
처음에 Lean은 다음과 같이 보여줍니다:
⊢ P ∧ Q → P
⊢ 뒤에 오는 모든 것은 현재의 증명 목표 (Proof goal)입니다.

이를 다음과 같이 생각할 수 있습니다: “이 타입에 해당하는 무언가를 구성하라(Construct something of this type).”

1단계: intro h
이는 h : P ∧ Q를 가정하며, 목표를 다음과 같이 변경합니다:
⊢ P
이제 우리는 h 안에 묶여 있는 다음의 증거들을 갖게 됩니다:

• P가 참이다
• Q가 참이다

2단계: 왼쪽 부분 추출하기
exact h.left
이는 P에 대한 증명을 추출합니다.
완료되었습니다.

이제 동일한 정리를 계산적(computationally) 관점에서 살펴보겠습니다. 이 정리는 다음과 동일합니다:
fun h => h.left
이는 단순히 다음과 같습니다: 쌍(pair)을 받아서 첫 번째 요소를 반환하라.
동일한 객체가 동시에 증명(proof)이자 프로그램(program)입니다. 이것이 바로 커리-하워드 대응 관계(Curry–Howard Correspondence)입니다.

Lean의 증명 목표는 증거에 대한 요청입니다
Lean을 이해하는 유용한 방법은 다음과 같습니다: Lean은 끊임없이 당신에게 증거를 요구하고 있습니다.
Lean이 다음과 같이 보여준다고 가정해 봅시다:
⊢ Sorted ys
이는 불리언(boolean) 체크가 아닙니다. Lean은 “이것이 참인가?”라고 묻는 것이 아닙니다. Lean은 “이것이 참이라는 증거를 구성할 수 있는가?”라고 묻고 있는 것입니다. 이 차이는 엄청나게 중요합니다.
일반적인 프로그래밍에서 정확성(correctness)은 종종 비형식적이고, 주석 속에 숨겨져 있거나, 테스트를 통해 검증됩니다. Lean에서 정확성은 타입 시스템(type system) 그 자체의 일부가 됩니다.

타입은 데이터의 형태뿐만 아니라 명세(specifications)를 표현할 수 있습니다
대부분의 프로그래머는 다음과 같은 타입에 익숙합니다:
sort : List Nat -> List Nat
이는 단지 다음과 같이 말할 뿐입니다: 입력: 리스트, 출력: 리스트. 정확성에 대해서는 아무것도 말하지 않습니다. 이 함수는 리스트를 뒤집거나, 섞거나, 쓰레기 값을 반환하거나, 항상 []를 반환할 수도 있습니다. 타입은 여전히 이를 허용할 것입니다.

이제 이것을 보십시오:
sort : ( xs : List Nat ) -> { ys : List Nat // Sorted ys ∧ Permutation xs ys }
이것은 모든 것을 바꿉니다. 이제 함수는 다음을 생성해야 합니다:

• 출력 리스트 ys
• ys가 정렬되었다는 증명
• ys가 xs와 정확히 동일한 요소들을 포함한다는 증명
  타입은 형태를 묘사하는 것을 멈추고 진리(truth)를 묘사하기 시작했습니다.

“Sorted”는 논리적 객체가 됩니다
하지만 Sorted는 어디에서 오는 걸까요? 그것 자체도 반드시 형식적으로 정의되어 있어야 합니다.

여기 단순화된 버전이 있습니다:

inductive Sorted : List Nat -> Prop
| nil : Sorted []
| single ( x : Nat ) : Sorted [ x ]
| cons ( x y : Nat ) ( xs : List Nat ) : x ≤ y -> Sorted ( y :: xs ) -> Sorted ( x :: y :: xs )

이것은 다음을 의미합니다:

• 빈 리스트는 정렬되어 있음 (Sorted)
• 요소가 하나인 리스트는 정렬되어 있음
• 더 큰 리스트는 다음 조건이 충족될 때 정렬되어 있음:
  • 첫 번째 요소가 두 번째 요소보다 작거나 같고 (≤)
  • 나머지 꼬리 부분 (tail)이 정렬되어 있음

이제 당신의 구현이 [1, 2, 3]을 반환한다고 가정해 봅시다. Lean은 다음을 위한 증거 (evidence)를 구성해야 합니다:
Sorted [1, 2, 3]

그 증명 (proof) 자체도 하나의 구조화된 객체입니다. 대략적으로 다음과 같습니다:

• 1 ≤ 2
• 2 ≤ 3
• 꼬리 부분이 정렬됨
  이 모든 것들이 재귀적으로 함께 조립됩니다.

함수가 잘못되었을 때는 어떤 일이 발생할까요?
만약 구현이 [3, 1, 2]를 반환한다고 가정해 봅시다. Lean은 이제 다음을 구성하려고 시도합니다:
Sorted [3, 1, 2]

하지만 Sorted의 정의에 따르면, 이는 결국 다음을 요구합니다:
proof(3 ≤ 1)

불가능합니다. 따라서 프로그램은 거부됩니다.

여기서 어떤 일이 일어났는지 주목하십시오. 우리는 다음과 같은 일을 하지 않았습니다:

• 테스트 실행
• 런타임 (runtime) 출력 검사
• 퍼징 (fuzzing) 입력
• 혹은 프로그램이 잘 작동하기를 기도함

대신에 다음과 같은 일이 일어났습니다:
구현이 요구되는 타입 (type)을 점유 (inhabit)하는 데 실패했습니다. 증명을 구성할 수 없었습니다. 따라서 프로그램은 유효하지 않았습니다.

근본적인 변화: 정당성(Correctness)이 구성(Construction)이 되다
이것이 Curry–Howard 대응 관계가 가능하게 한 개념적 도약입니다.

전통적으로:

• 프로그램은 동작적인 산물 (operational artifacts)이었고,
• 증명은 인간의 추론 산물 (human reasoning artifacts)이었습니다.

Curry–Howard는 이들이 동일한 구조를 공유한다는 것을 보여주었습니다. 그 통찰은 다음과 같은 분야로 이어졌습니다:

• 증명 보조기 (proof assistants)
• 의존 타입 프로그래밍 (dependently typed programming)
• 형식적으로 검증된 커널 (formally verified kernels)
• 검증된 컴파일러 (verified compilers)
• 기계가 검증하는 수학 (machine-checked mathematics)
• 암호학적 검증 시스템 (cryptographic verification systems)

핵심적인 변화는 이것입니다:
증명은 단순히 논증하는 것이 아닙니다. 그것은 구체적인 계산 객체 (computational object)입니다. 그리고 Lean에서는 프로그램을 작성하는 것과 그것이 올바름을 증명하는 것이 동일한 행위가 될 수 있습니다.

맺음말
사람들이 처음으로 "명제는 타입이다 (propositions are types)", "증명은 프로그램이다 (proofs are programs)"라는 말을 들으면, 종종 추상적인 수학적 시처럼 들리곤 합니다. 하지만 Lean은 이 아이디어를 구체화합니다.

• 정리 (theorem)는 타입 (type)이 됩니다.
• 증명 (proof)은 값 (value)이 됩니다.
• 함수 (function)는 논리적 함축 (logical implication)이 됩니다.
• 그리고 타입 체킹 (type checking)은 증명 검증 (proof verification)이 됩니다.

그 결과, 정확성 (correctness)이 단순히 사후에 문서화되거나 테스트되는 것이 아니라, 프로그램 그 자체의 일부가 되는 시스템이 탄생합니다. 이것이 바로 커리-하워드 대응 관계 (Curry–Howard correspondence)의 진정한 의의입니다. 즉, 그 자체를 위한 철학이 아니라 논리 (logic)와 실행 가능한 시스템 (executable systems) 사이를 잇는 가교 역할을 하는 것입니다. 그리고 일단 Lean 내부에서 이를 목격하고 나면, 다시 이전의 방식으로 돌아가기는 어렵습니다.