Lean 4와 의존 타입으로 구현한 Zero-Cost POSIX 소켓: 혁신과 한계

“가장 좋은 런타임 체크는 아예 실행되지 않는 체크다.”

엔지니어라면 누구나 공감할 만한 매력적인 문장입니다. 최근 해커뉴스에서 아주 흥미로운 아티클을 하나 읽었습니다. POSIX 소켓의 상태 머신(State Machine)을 Lean 4의 의존 타입(Dependent Types)을 활용해 컴파일 타임에 완벽하게 검증한다는 내용이었죠.

15년 넘게 시스템 프로그래밍과 백엔드 인프라를 다뤄온 입장에서, 소켓 상태 관리로 인해 발생하는 수많은 런타임 버그들은 늘 골칫거리였습니다. C 언어에서는 개발자가 매뉴얼을 달달 외워야 했고, Python이나 Go 같은 언어들은 런타임 오버헤드를 감수하며 매번 상태를 체크해야 했습니다. Rust가 Typestate 패턴을 통해 이 문제를 컴파일 타임으로 끌어올렸지만, 이번에 소개된 Lean 4의 접근 방식은 한 걸음 더 나아가 수학적 증명 의 영역으로 이를 가져갔습니다.

오늘은 이 아티클이 제시하는 기술적 혁신이 무엇인지 깊게 파헤쳐보고, 동시에 현업 엔지니어의 시각에서 보이는 명확한 한계점들을 짚어보려 합니다.

상태 머신을 타입 시스템에 구워 넣기

POSIX 소켓 API는 본질적으로 상태 머신입니다. 소켓을 생성하고(fresh), 바인딩하고(bound), 수신 대기 상태로 만들고(listening), 연결한 뒤(connected), 마지막에 닫아야(closed) 합니다. 순서가 어긋나면 에러가 발생하죠.

Lean 4는 이 5개의 상태를 다음과 같이 Inductive type으로 정의합니다.

inductive SocketState where
  | fresh
  | bound
  | listening
  | connected
  | closed
deriving DecidableEq

여기서 핵심은 Socket 구조체가 이 상태를 Phantom parameter로 가진다는 점입니다.

structure Socket (state : SocketState) where
  protected mk :: raw : RawSocket -- opaque FFI handle

이 state 파라미터는 오직 타입 레벨에서만 존재합니다. 런타임에는 완전히 소거(erased)되어 C 언어의 원시 파일 디스크립터 포인터와 정확히 동일한 메모리 레이아웃을 가집니다. 즉, 추상화로 인한 런타임 오버헤드가 Zero 라는 뜻입니다.

의존 타입의 마법: by decide

이 아티클에서 가장 감탄했던 부분은 이중 종료(Double-close)를 방지하는 로직입니다.

def close (s : Socket state) (_h : state ≠ .closed := by decide) : IO (Socket .closed)

close 함수는 두 번째 파라미터로 _h를 받습니다. 이는 현재 상태가 .closed가 아니라는 논리적 증명(Proof) 입니다. Lean 4의 컴파일러는 by decide 전술(Tactic)을 통해 이 증명을 자동으로 수행합니다.

만약 이미 닫힌 소켓을 다시 닫으려 한다면, 컴파일러는 .closed ≠ .closed라는 명제를 증명해야 하는데 이는 논리적으로 거짓이므로 컴파일을 거부합니다. 런타임 분기문(Branch)이나 플래그(Flag) 없이, 수학적 증명을 통해 버그를 원천 차단하는 것입니다. 코드를 생성할 때는 이 증명 과정이 흔적도 없이 사라져 순수 C 코드와 동일한 속도로 실행됩니다.

하지만, 현실은 그렇게 호락호락하지 않다

이론적으로는 무척 아름답습니다. 하지만 해커뉴스 스레드와 제 개인적인 경험을 비추어 볼 때, 이 방식이 당장 프로덕션에 도입될 수 있을지에는 강한 의문이 듭니다.

  • 선형 타입(Linear Typing)의 부재: 해커뉴스 유저들이 가장 날카롭게 지적한 부분입니다. Rust의 Typestate 패턴이 실전에서 강력한 이유는 소유권(Ownership) 모델이 뒷받침되기 때문입니다. 위 Lean 4 예제에서는 let s = bind s 형태로 변수를 섀도잉(Shadowing)하여 이전 상태를 가리지만, 만약 이전 상태의 소켓 레퍼런스를 리스트나 다른 변수에 저장해두었다면 어떻게 될까요? Lean 4는 선형 타입 시스템을 기본적으로 강제하지 않기 때문에, 오래된 래퍼런스(Aliasing)를 통해 유효하지 않은 상태의 소켓을 다시 호출하는 끔찍한 상황을 막을 수 없습니다. 또한 소켓을 닫지 않고 그냥 버리는(Dropping) 암묵적 약화(Implicit weakening) 문제도 여전히 남아있습니다.

  • C 언어 UB에 대한 오해: 아티클 원문에서는 바인딩되지 않은 소켓에 send를 호출하는 것이 C에서 Undefined Behavior라고 언급했지만, 이는 엄밀히 틀린 말입니다. C 언어 스펙상의 UB가 아니라, 단순히 OS 커널이 -errno (예: EBADF)를 반환하는 에러 상황일 뿐입니다. 마케팅적인 수사(AI-generated 느낌이 나는 “No X. No Y. Just pure Z.”)를 위해 약간 과장된 면이 있습니다.

  • 비동기 상태의 복잡성: 현업에서 네트워크 프로그래밍을 해보면 상태가 항상 동기적으로 딱딱 떨어지지 않습니다. Non-blocking 소켓에서 connect를 호출하면 EINPROGRESS가 떨어집니다. 연결이 진행 중인지, 실패했는지 알 수 없는 림보 상태에 빠지죠. 외부 요인에 의해 밑바닥부터 상태가 변하는(Mutating out from under the program) 실제 시스템의 복잡성을 이런 엄격한 논리 프로그래밍으로 어떻게 우아하게 풀어낼 수 있을지는 아직 미지수입니다.

결론

이 아티클은 의존 타입(Dependent Types)이 단순한 수학적 증명 도구를 넘어, 시스템 프로그래밍의 안정성을 극대화하는 데 어떻게 사용될 수 있는지 보여주는 훌륭한 PoC(Proof of Concept)입니다.

하지만 선형 타입 시스템의 결합 없이는 실무에서 발생하는 복잡한 Aliasing 문제를 해결하기 어렵습니다. 개인적으로는 이 접근법이 당장 C나 Rust를 대체할 것이라 보진 않습니다. 그럼에도 불구하고, 런타임 오버헤드 없이 컴파일러를 수학적 증명기로 활용해 프로토콜 규격을 검증한다는 아이디어 자체는 시스템 언어가 나아가야 할 흥미로운 미래를 제시하고 있습니다.

언젠가 Rust의 소유권 모델과 Lean 4의 의존 타입이 결합된 언어가 나온다면, 그때는 정말로 “완벽하게 안전한” 네트워크 프로그래밍이 가능해질지도 모르겠습니다.

References: