Lean 4: '완벽하게 만들어갈 수 있는' 프로그래밍 언어라는 개념

프로그래밍 언어가 '완벽해질 수 있다'는 건 무슨 뜻일까요?

보통 프로그래밍 언어를 고를 때 "이 언어가 빠른가?", "생태계가 좋은가?" 같은 걸 따지잖아요. 그런데 여기 조금 다른 질문을 던지는 언어가 있어요. "내 코드가 정말로 맞다는 걸 수학적으로 증명할 수 있는가?" 바로 Lean 4 이야기인데요.

Lean은 원래 마이크로소프트 리서치에서 시작된 정리 증명기(theorem prover)예요. 이게 뭐냐면, 수학에서 "이 명제가 참이다"를 증명하듯이, 코드가 의도한 대로 동작한다는 걸 논리적으로 증명할 수 있게 해주는 도구거든요. 그런데 Lean 4에 와서는 단순한 증명 도구를 넘어서 범용 프로그래밍 언어로도 쓸 수 있게 진화했어요.

"완벽하게 만들어갈 수 있는 언어(Perfectable Language)"라는 표현은 Lean의 핵심 철학을 잘 담고 있어요. 처음부터 완벽한 코드를 작성하라는 게 아니라, 코드를 작성한 뒤에 점진적으로 증명을 추가하면서 완벽에 가까워질 수 있다는 뜻이에요.

어떻게 동작하는 건가요?

일반적인 프로그래밍에서는 테스트를 작성해서 "이 입력을 넣으면 이 출력이 나온다"를 확인하죠. 하지만 테스트는 결국 유한한 케이스만 확인할 수 있어요. 반면 Lean에서는 타입 시스템 자체가 증명 시스템이에요. 의존 타입(dependent type)이라는 걸 사용하는데요, 이게 뭐냐면 타입이 값에 의존할 수 있다는 뜻이에요.

예를 들어볼게요. 일반 언어에서 "정수 리스트를 정렬하는 함수"를 만들면 반환 타입은 그냥 List<Int>예요. 하지만 Lean에서는 반환 타입에 "이 리스트는 정렬되어 있고, 원래 리스트와 같은 원소를 가진다"는 조건을 붙일 수 있어요. 컴파일러가 이 조건이 실제로 충족되는지 검사해주기 때문에, 만약 정렬 로직에 버그가 있으면 아예 컴파일이 안 돼요.

이런 접근의 핵심은 점진성이에요. 처음에는 그냥 동작하는 코드를 작성하고, 나중에 시간이 될 때 증명을 하나씩 추가해가면 돼요. 마치 집을 짓고 나서 한 방씩 인테리어를 하는 것과 비슷하달까요. 처음부터 모든 걸 증명할 필요가 없다는 거죠.

기존 방식과 뭐가 다른가요?

비슷한 철학을 가진 언어들이 몇 개 있어요. Coq, Agda, Idris 같은 언어들인데요. Coq는 수학 증명 쪽에서 가장 오래된 역사를 갖고 있고, Idris는 범용 프로그래밍에 좀 더 초점을 맞추고 있어요.

그런데 Lean 4가 이 중에서 주목받는 이유가 있어요. 첫째, 성능이 꽤 좋아요. Lean 4는 C로 컴파일되기 때문에 실행 속도가 빠르고, 참조 카운팅 기반 메모리 관리를 해서 가비지 컬렉터 없이도 효율적으로 돌아가요. 둘째, 메타프로그래밍이 강력해요. Lean의 문법이나 기능을 Lean 자체로 확장할 수 있어서, 사용자가 자기만의 DSL(도메인 특화 언어)을 만들기도 쉬워요. 셋째, 마이크로소프트의 지원 아래 수학 라이브러리(Mathlib)가 빠르게 성장하고 있어서, 실제 수학 연구에서도 많이 사용되고 있어요.

최근에는 AI와 수학 증명의 결합에서도 Lean이 핫해요. Google DeepMind의 AlphaProof가 수학 올림피아드 문제를 풀 때 Lean을 활용했다는 게 알려지면서, AI 연구 커뮤니티에서도 관심이 부쩍 늘었거든요.

한국 개발자에게 어떤 의미가 있을까요?

솔직히 말하면, 당장 실무 프로젝트에서 Lean 4로 서버를 짜거나 앱을 만들 일은 많지 않아요. 하지만 배워둘 가치는 분명히 있어요.

우선, 함수형 프로그래밍과 타입 시스템에 대한 이해가 깊어져요. TypeScript나 Rust의 타입 시스템도 결국 이런 정리 증명 이론에서 영감을 받은 건데, Lean을 배우면 타입이라는 개념을 더 근본적으로 이해할 수 있게 돼요. 둘째, 금융이나 블록체인처럼 코드의 정확성이 치명적인 분야에서는 형식 검증(formal verification)의 수요가 점점 늘고 있어요. 스마트 컨트랙트의 버그가 수백억 원의 손실로 이어지는 걸 생각하면, 코드가 맞다는 걸 수학적으로 보장할 수 있다는 건 꽤 매력적이죠.

또 하나, 최근 AI가 코드를 생성하는 시대에 "이 코드가 정말 맞나?"를 검증하는 도구로서 형식 검증의 가치가 올라가고 있어요. AI가 만든 코드를 Lean으로 검증하는 파이프라인도 연구되고 있거든요.