테스트로는 '버그가 없다'를 증명할 수 없어요
프로그래밍 대가 다익스트라가 남긴 유명한 말이 있어요. '테스트는 버그의 존재를 보여줄 뿐, 버그가 없음을 보여주지는 못한다.' 무슨 뜻이냐면, 우리가 아무리 테스트 케이스를 100개, 1000개 만들어서 다 통과시켜도, 그건 '우리가 확인한 경우엔 문제없다'는 것뿐이지 '모든 경우에 문제없다'는 보장은 아니라는 거예요. 우리가 미처 생각 못 한 입력 하나에서 터질 수 있으니까요.
그럼 '모든 경우에 확실히 옳다'를 증명하는 방법은 없을까요? 있어요. 바로 형식 검증(Formal Verification)이에요. 이건 프로그램이 명세(원하는 동작)를 만족한다는 걸 수학의 증명처럼 논리적으로 완전하게 보여주는 방법이에요. 테스트가 '많이 두들겨보기'라면, 형식 검증은 '수학적으로 못을 박기'인 셈이죠. 그리고 이 형식 검증을 도와주는 도구 중에 요즘 가장 뜨거운 게 바로 Lean이에요.
Lean이 뭐냐면
Lean은 두 얼굴을 가진 도구예요. 한편으로는 프로그래밍 언어이고, 다른 한편으로는 정리 증명기(theorem prover)예요. 정리 증명기란 수학 정리를 사람이 한 줄씩 논리로 증명해나가면, 컴퓨터가 그 증명에 빈틈이 없는지 엄격하게 검사해주는 프로그램이에요. 사람이 '여기까진 맞지?' 하면 컴퓨터가 '응 맞아' 또는 '아니 거기 논리가 비었어'라고 깐깐하게 채점해주는 조교라고 생각하면 돼요.
Lean의 핵심 아이디어는 '명제는 곧 타입이고, 증명은 곧 프로그램이다'라는 거예요(커리-하워드 대응이라고 불러요). 좀 어렵게 들리죠? 쉽게 말하면, '1+1=2가 참이다'라는 명제를 증명하는 건, 그 타입을 만족하는 값(프로그램)을 하나 만들어내는 것과 똑같다는 거예요. 그래서 Lean에서는 코드를 짜는 것과 수학을 증명하는 것이 근본적으로 같은 행위가 돼요.
실제로는 이렇게 생겼어요. 어떤 정리를 증명할 때 theorem으로 선언하고, 그 아래에서 택틱(tactic)이라는 명령들을 써서 증명을 조금씩 진행해요. intro로 가정을 가져오고, simp로 식을 정리하고, exact로 결론을 맺는 식이죠. 마치 수학 문제를 풀 때 '양변에 2를 곱하고, 이항하고, 정리하면...' 하는 과정을 컴퓨터가 검증 가능한 명령으로 옮긴 거예요.
다른 도구들과 어떻게 다를까
형식 검증 도구는 Lean 말고도 오래된 강자들이 있어요. Coq는 학계에서 오래 쓰여왔고 CompCert(검증된 C 컴파일러) 같은 대형 성과를 냈어요. Isabelle은 seL4라는 완전히 검증된 운영체제 커널을 증명하는 데 쓰였고요. Agda는 함수형 프로그래밍과 증명을 결합한 쪽으로 유명해요.
Lean이 이들 사이에서 빠르게 주목받는 이유는 두 가지예요. 하나는 문법이 비교적 현대적이고 프로그래머에게 친숙하다는 점, 다른 하나는 mathlib이라는 어마어마한 수학 라이브러리예요. 전 세계 수학자와 개발자들이 힘을 모아 해석학, 대수학, 위상수학 같은 방대한 수학을 Lean으로 형식화해놨는데, 이게 있으면 매번 밑바닥부터 증명할 필요 없이 검증된 정리들을 레고 블록처럼 가져다 쓸 수 있어요.
한국 개발자에게
형식 검증은 예전엔 '학계에서나 하는 것'이었지만, 지금은 실무 영역이 넓어지고 있어요. 특히 블록체인 스마트 컨트랙트처럼 버그 하나가 곧 수백억 원 손실로 이어지는 분야, 그리고 암호 프로토콜이나 항공·의료처럼 사람 목숨이 걸린 안전 필수(safety-critical) 시스템에서 형식 검증 수요가 커지고 있어요.
당장 웹 서비스 만드는 데 Lean을 쓸 일은 없을 거예요. 하지만 '내 코드가 옳다는 걸 어떻게 논리적으로 보장할까'라는 사고방식 자체가, 평소 코드를 더 엄밀하게 설계하는 감각을 길러줘요. 타입 시스템이 왜 강력한지, 왜 요즘 언어들이 타입에 집착하는지도 훨씬 깊이 이해하게 되고요. 관심 있다면 튜토리얼 1편부터 가볍게 따라가보는 걸 추천해요.
마무리
핵심은 이거예요. 테스트가 '충분히 확인했다'라면, 형식 검증은 '수학적으로 증명했다' — 이 차이가 어떤 시스템에서는 생사를 가른다는 거죠. 여러분은 '버그가 없음을 증명'해야 할 만큼 중요한 코드를 짜본 적 있으세요? 만약 그런 상황이라면 형식 검증이라는 무기를 꺼내볼 만할까요?
🔗 출처: Hacker News)