Lean 4의 타입 시스템으로 소켓 프로그래밍 실수를 컴파일 타임에 잡는 방법

소켓 프로그래밍, 순서 틀리면 바로 크래시

네트워크 프로그래밍을 해본 분이라면 소켓(socket) API의 까다로움을 아실 거예요. socket() → bind() → listen() → accept() 이 순서를 정확히 지켜야 하는데, 순서를 하나라도 틀리면 런타임에 에러가 나거든요. 컴파일할 때는 멀쩡하게 통과하고, 실행해봐야 "아 이거 순서가 잘못됐구나" 하고 알게 되는 거죠. POSIX 소켓 API가 원래 C로 설계됐기 때문에 이런 상태 전이(state transition)를 타입 레벨에서 강제할 방법이 없었어요.

최근 한 개발자가 Lean 4라는 언어의 타입 시스템을 활용해서 이 문제를 아예 컴파일 타임에 잡아내는 방법을 공개했는데요, 정말 흥미로운 접근이에요.

핵심 아이디어: 소켓의 "상태"를 타입으로 표현하기

이게 뭐냐면, 소켓이 지금 어떤 상태인지를 타입 자체에 녹여넣는 거예요. 예를 들어 소켓이 막 생성된 상태, bind된 상태, listen 중인 상태, 연결된 상태 — 이런 것들을 각각 다른 타입으로 만드는 거죠.

일반적인 프로그래밍에서는 소켓이 그냥 하나의 타입이에요. Socket 타입 하나로 모든 상태를 다 표현하죠. 그래서 아직 bind도 안 한 소켓에 accept()를 호출해도 컴파일러는 아무 문제 없다고 판단해요. 하지만 Lean 4에서는 Socket Created, Socket Bound, Socket Listening 같은 식으로 소켓의 상태가 타입에 포함되니까, accept() 함수가 "나는 Socket Listening 타입만 받을 수 있어"라고 선언할 수 있어요. 잘못된 순서로 호출하면? 타입이 안 맞으니까 컴파일 자체가 안 되는 거예요.

이걸 전문 용어로 "상태 머신을 타입으로 인코딩한다"고 하는데요, 쉽게 비유하면 레고 블록처럼 맞는 모양끼리만 끼울 수 있게 만든 거라고 보시면 돼요.

"제로 코스트"라는 게 진짜 가능해?

여기서 "제로 코스트(zero-cost)"가 핵심 포인트예요. 이런 타입 레벨의 안전장치를 추가하면 보통은 런타임 오버헤드가 생기지 않을까 걱정하잖아요. 그런데 Lean 4의 타입 시스템에서 이 상태 정보는 순전히 컴파일 타임에만 존재하고, 실제로 컴파일된 코드에서는 완전히 사라져요. 마치 Rust의 제로 코스트 추상화(zero-cost abstraction)와 비슷한 개념이에요. 타입 검사가 끝나면 그 정보는 더 이상 필요 없으니 바이너리에 아무런 흔적도 남기지 않는 거죠.

이 접근 방식에서는 의존 타입(dependent types)이라는 개념을 활용하는데요, 이건 값에 따라 타입이 달라질 수 있는 타입 시스템이에요. 일반적인 제네릭이 "어떤 타입이든 받을 수 있어"라는 거라면, 의존 타입은 "이 특정 값을 가진 것만 받을 수 있어"까지 표현할 수 있는 훨씬 강력한 도구예요. Lean 4가 바로 이 의존 타입을 지원하는 언어 중 하나이고요.

업계에서의 위치: 타입 안전성 트렌드

이 아이디어 자체가 완전히 새로운 건 아니에요. Rust에서도 typestate 패턴이라고 해서 비슷한 접근을 시도할 수 있고, Haskell에서도 인덱스드 모나드(indexed monad)를 활용해서 상태 전이를 타입으로 표현하는 연구가 있었거든요. 하지만 Lean 4는 의존 타입을 기본으로 지원하기 때문에 이런 패턴을 훨씬 자연스럽고 깔끔하게 표현할 수 있다는 장점이 있어요.

특히 Lean 4는 원래 수학 정리 증명기(theorem prover)로 시작했지만, 최근에는 범용 프로그래밍 언어로서의 가능성을 보여주고 있어요. 이번 소켓 API 예제는 "실용적인 시스템 프로그래밍에도 정리 증명기의 타입 시스템이 도움이 될 수 있다"는 걸 보여주는 좋은 사례이기도 하고요.

Idris 2라는 언어도 비슷한 방향으로 프로토콜의 상태 머신을 타입으로 표현하는 연구를 진행해왔는데, Lean 4 쪽에서 이렇게 구체적인 POSIX 소켓 예제를 보여준 건 의미가 있어요.

한국 개발자에게 주는 시사점

솔직히 말하면, 당장 실무에서 Lean 4로 소켓 프로그래밍을 할 일은 거의 없을 거예요. 하지만 이 글에서 얻어갈 수 있는 건 있어요.

첫째, 타입 시스템으로 버그를 예방한다는 사고방식이에요. TypeScript에서 유니온 타입이나 discriminated union을 잘 활용하는 것도 같은 맥락이거든요. "런타임에서 잡을 버그를 컴파일 타임으로 끌어올린다"는 발상은 어떤 언어를 쓰든 적용할 수 있는 원칙이에요.

둘째, Lean 4에 대한 관심이 최근 AI와 수학 분야에서 크게 늘고 있어요. 메타(Meta)가 Lean 4를 활용한 수학 증명 자동화 연구를 진행하고 있고, 프로그래밍 언어 이론에 관심 있는 분들에게는 배워둘 가치가 충분해요.