소프트웨어의 정확성을 수학적으로 증명하는 의존형 타입 언어(dependently-typed language)는 오랫동안 이상적인 개념으로 여겨져 왔습니다. 코크(Coq), 린(Lean)과 같은 언어는 일반적인 프로그래밍 언어에서 주석으로만 남거나 팀 규모가 커지면서 사라지기 쉬운 미묘한 불변성(invariants)까지 타입 시스템으로 인코딩하고 강제할 수 있는 잠재력을 가집니다. 이는 시스템의 구성 요소들이 정확히 맞아떨어지도록 보장하여, 나중에 발견될 수 있는 복잡한 오작동이나 버그를 사전에 방지하는 데 도움을 줍니다.
하지만 이러한 강력한 타입 시스템에는 엄청난 '증명 노력(proof effort)'이라는 대가가 따랐습니다. 과거 seL4 프로젝트의 사례에서 보듯이, 엔지니어들은 설계 및 구현 시간의 약 10배를 증명에 할애했으며, C 코드보다 20배 많은 증명 코드를 작성해야 했습니다. 이는 의존형 타입 언어가 극도로 틈새시장에 머무르게 한 주요 원인이었습니다. SMT 솔버(Satisfiability Modulo Theories solver)를 이용한 자동화 시도도 있었지만, 복잡한 경우 솔버가 무한정 실행되거나 예측 불가능한 결과를 내놓는 등 한계가 명확했습니다. 결국 개발자들은 솔버를 '만족시키는' 육감 같은 능력을 키워야 했고, 이는 문제를 신비주의 영역으로 밀어 넣는 결과를 초래했습니다.
최근 대규모 언어모델(LLM)의 등장은 이러한 증명 자동화의 판도를 바꿀 잠재력을 보여주고 있습니다. LLM은 '증명 무관성(proof irrelevance)'이라는 개념과 결합하여, 증명의 내용보다는 증명의 존재 자체에 초점을 맞춰 자동화의 효율성을 극대화할 수 있습니다. 즉, LLM이 복잡한 증명 과정을 대신 수행하여 개발자의 부담을 획기적으로 줄여주는 것입니다. 이로 인해 '증명 엔지니어링(proof engineering)'과 같은 복잡한 관리 작업의 필요성도 크게 줄어들 수 있습니다. 저자는 이러한 가능성을 탐구하기 위해 린(Lean) 언어로 Zstandard 압축 해제기를 구현하는 실험을 진행했으며, LLM이 타입 검사기를 과부하 시키지 않으면서도 증명 작업을 효율적으로 처리할 수 있음을 확인했습니다. 이는 의존형 타입 시스템이 실용적인 개발 환경에서 훨씬 더 널리 사용될 수 있는 길을 열어줄 것입니다. 궁극적으로는 소프트웨어의 신뢰성과 안정성을 극대화하여, 버그로 인한 사회적, 경제적 손실을 줄이는 데 크게 기여할 수 있습니다.