'테스트는 버그가 있다는 건 보여줄 수 있어도, 없다는 건 증명하지 못한다.' 다익스트라의 유명한 말인데요. 그래서 컴퓨터 과학자들은 오래전부터 꿈을 꿨어요. 프로그램이 올바르다는 걸 수학 정리처럼 증명해버리자는 거죠. 이걸 '형식 검증(formal verification)'이라고 해요. 이게 뭐냐면, 몇 가지 입력을 넣어보고 결과를 확인하는 테스트와 달리, 가능한 모든 경우에 대해 프로그램이 명세대로 동작한다는 걸 논리적으로 증명하는 접근이에요. 그런데 1970년대 후반, 이 꿈에 정면으로 찬물을 끼얹은 논문이 나왔거든요. De Millo, Lipton, Perlis가 쓴 '사회적 과정과 정리 및 프로그램의 증명'이라는 고전인데, 50년 가까이 지난 지금 이 논문을 다시 꺼내 읽으며 그 예언이 맞았는지 따져보는 글이 나와서 소개해요.
원조 반대론의 논리: 증명은 사회적 활동이다
이 논문의 주장이 정말 흥미로워요. 수학의 증명이 믿을 만한 이유는 증명 그 자체가 완벽해서가 아니라, 그걸 둘러싼 '사회적 과정' 덕분이라는 거예요. 수학자가 증명을 발표하면 동료들이 읽고, 세미나에서 물어뜯고, 심사에서 걸러지고, 다른 연구에 인용되면서 검증되잖아요. 이 과정에서 틀린 증명은 탈락하고 살아남은 증명만 신뢰를 얻는 거죠. 그런데 프로그램의 정확성 증명은 어떨까요? 수백 페이지짜리 기계적인 논리 나열이라 아무도 읽고 싶어 하지 않아요. 읽는 사람이 없으면 사회적 검증 과정도 없고, 검증 과정이 없으면 신뢰도 생기지 않는다. 그러니 프로그램 검증은 수학 증명 같은 지위를 얻지 못할 거라는 논리예요. 당시 검증 연구자들이 발끈할 만큼 도발적인 주장이었죠.
50년이 지난 지금, 예언은 맞았을까요
절반은 맞고 절반은 틀렸다고 봐야 할 것 같아요. 맞은 부분부터 보면, 일반적인 소프트웨어 개발에서 형식 검증은 여전히 비주류예요. 우리 대부분은 테스트 코드를 짜지 증명을 쓰진 않잖아요. 논문이 지적한 비용 문제, 그러니까 증명에 드는 노력이 코드 작성보다 훨씬 크다는 문제는 지금도 유효해요.
그런데 틀린 부분이 더 흥미로워요. 논문이 예상 못 한 반전이 있었거든요. 바로 증명을 사람이 아니라 기계가 검사하는 시대가 온 거예요. Coq(지금은 Rocq), Isabelle, Lean 같은 증명 보조 도구들은 증명의 모든 단계를 작은 커널 프로그램이 기계적으로 검사해요. '아무도 안 읽어서 신뢰할 수 없다'는 논리가, 기계가 대신 읽어주면서 무너진 거죠. 실제 성과도 나왔어요. seL4라는 운영체제 마이크로커널은 C 코드 전체가 명세대로 동작한다는 게 완전히 증명됐고요. 검증된 C 컴파일러인 CompCert에는 유명한 일화가 있는데, 컴파일러 버그를 찾는 퍼징 도구가 GCC와 LLVM에서 수백 개의 버그를 찾아내는 동안 CompCert의 검증된 부분에서는 단 하나도 찾지 못했어요. AWS 같은 회사는 TLA+라는 명세 도구로 분산 시스템 설계를 검증해서 미묘한 동시성 버그를 출시 전에 잡아내고 있고요.
그리고 가장 아이러니한 반전이 있어요. Lean의 수학 라이브러리인 mathlib 커뮤니티에는 수많은 수학자와 개발자가 참여해서 형식 증명을 함께 작성하고 리뷰하는데요. 이건 논문이 말한 바로 그 '사회적 과정'이에요. 형식 증명은 사회적 과정을 가질 수 없다고 했는데, 형식 증명 위에 사회적 과정이 새로 생겨버린 거죠.
그래도 남아 있는 진짜 문제
다만 논문의 지적 중 지금도 뼈아픈 게 하나 있어요. 명세(specification) 문제인데요. 아무리 완벽하게 증명해도 '올바른 것을 증명했는가'는 별개의 문제예요. 명세 자체가 잘못됐으면, 증명은 잘못된 프로그램에 대한 완벽한 보증서가 될 뿐이거든요. 이건 기계가 해결해줄 수 없는, 여전히 사람의 판단 영역이에요.
한국 개발자에게 주는 시사점
형식 검증 전부를 배울 필요는 없지만, 가벼운 입구는 충분히 실용적이에요. 분산 시스템을 설계한다면 TLA+로 핵심 프로토콜만 모델링해봐도 동시성 버그를 코드 짜기 전에 발견할 수 있고요. 속성 기반 테스트(property-based testing)는 테스트와 증명의 중간쯤 되는 기법이라 진입 장벽이 낮아요. 요즘은 AI가 증명 작성을 도와주면서 문턱이 빠르게 낮아지고 있어서, 지금이 관심 가지기 좋은 시점이기도 해요.
정리하면
50년 전의 반대론은 형식 검증을 죽이지 못했지만, 형식 검증이 어디서 어떻게 쓰여야 하는지를 더 선명하게 만들어줬어요. 여러분의 프로젝트에서 '테스트만으로는 부족하다'고 느꼈던 순간이 있나요? 있었다면 어떤 부분이었는지 궁금해요.
🔗 출처: Hacker News