Proof Searching in DepC - CppCon 2025 라이트닝 토크
📺 원본 영상: Lightning Talk: Proof Searching in DepC - Raffaele Rossi - CppCon 2025 🎙️ 채널: CppCon 📅 정리 일자: 2026-05-15 ⚠️ Note: 본 리포트는 영상의 음성을 텍스트로 변환(STT)하여 정리한 것입니다. 화면에 표시된 자료(코드, 슬라이드 등)는 포함되지 않을 수 있습니다.
개요
이 라이트닝 토크는 Maven의 테크 리드이자 DepC(Dependent C) 언어의 기여자인 Raffaele Rossi가 발표한 세션으로, 의존 타입 시스템(Dependent Type System)을 갖춘 언어 DepC의 컴파일러에 구현된 증명 탐색(Proof Search) 알고리즘을 소개한다. 약 3분 남짓의 짧은 발표임에도 불구하고, 타입 이론의 핵심 개념부터 실제 컴파일러 내부 구현까지 밀도 높게 다루고 있다. 타입 검사와 증명 탐색의 차이를 출발점으로 삼아, 컴파일러가 프로그래머를 대신해 런타임 안전성을 정적으로 보장하는 방식을 설명한다.
타입 검사와 증명 탐색 - 두 가지 근본적인 질문
타입 이론(Type Theory)에는 컴파일러가 답해야 하는 두 가지 근본적인 질문이 존재한다. 첫 번째는 우리 모두에게 익숙한 **타입 검사(Type Checking)**다. “표현식 x가 주어졌을 때, 그것이 타입 t를 가지는가?”라는 질문으로, 오늘날 대부분의 컴파일러가 일상적으로 수행하는 작업이다. 두 번째는 이와 정반대 방향의 질문인 **증명 탐색(Proof Searching)**이다. “타입 t가 주어졌을 때, 컴파일러가 그 타입의 값을 스스로 찾아낼 수 있는가?”라는 물음이다.
강연자는 청중이 가질 법한 자연스러운 의문을 미리 짚고 넘어간다. “값을 찾는 것인데, 왜 ‘값 탐색(Value Search)‘이 아니라 ‘증명 탐색(Proof Search)‘이라고 부르는가?” 이 명칭의 근거는 **커리-하워드 대응(Curry-Howard Correspondence)**에 있다. 이 원리는 타입과 논리적 명제가, 그리고 값과 그 명제의 증명이 서로 동형(isomorphic)임을 말한다. 즉, 어떤 타입의 값을 찾는 행위는 곧 해당 타입이 나타내는 명제를 증명하는 행위와 동일하다는 것이다. 강연자는 이 개념 자체에 대한 상세한 설명은 별도로 검색해볼 것을 권하며, 핵심 주제인 DepC의 구현으로 빠르게 이동한다.
DepC 언어와 의존 타입
강연자는 DepC(Dependent C)의 기본적인 프로그램 구조를 소개하는 것으로 본론을 시작한다. 우선 눈에 띄는 점은 argc와 argv의 관계다. C와 C++ 프로그래머에게 이 두 매개변수는 단순히 관례적으로 함께 전달되는 값이지만, DepC에서는 argv가 argc에 **런타임에 의존(depends on)**한다는 사실이 타입 시스템 수준에서 명시적으로 표현된다. 이것이 바로 의존 타입(Dependent Type)의 핵심이다. 타입이 값에 의존할 수 있으므로, argv의 타입은 “길이가 argc인 배열에 대한 포인터”로 정밀하게 기술된다.
01:12 - 기본 DepC 프로그램 예제 - argc/argv 의존 타입 관계를 보여주는 코드
경계 검사 - 증명 탐색의 실전 사례
단순한 예제를 넘어, 강연자는 libc의 puts 함수를 선언하고 이를 통해 프로그램의 첫 번째 인자(argv[1])를 출력하는 코드를 작성한다. 여기서 DepC 컴파일러는 즉각 불만을 표시한다. 1이 argv의 유효한 인덱스 범위 내에 있다는 것을 증명하지 못했기 때문이다. 일반적인 C/C++ 컴파일러라면 조용히 통과시키고 런타임에 미정의 동작(Undefined Behavior)을 허용할 부분을, DepC는 컴파일 타임에 정적으로 차단한다.
그렇다면 이 증명을 어떻게 제공하는가? 가장 자연스러운 방법은 if (1 < argc) 조건을 추가하는 것이다. 이 분기의 then 블록 안에서 컴파일러는 1 < argc라는 사실이 성립함을 알게 되고, 이를 바탕으로 argv[1] 접근이 경계 안에 있음을 자동으로 증명한다. 바로 이 과정이 증명 탐색 알고리즘이 동작하는 순간이다. 컴파일러가 현재의 타입 컨텍스트(type context)를 검토하여 필요한 증명 조각을 스스로 조립해낸다.
01:43 - if (1 < argc) 조건을 통해 배열 경계 증명을 제공하는 코드 예제
강연자는 현실적인 대안도 함께 소개한다. 증명이 너무 복잡하거나 귀찮을 때, 프로그래머가 컴파일러에게 “그냥 믿어달라”고 요청하는 일종의 탈출구(escape hatch)가 존재한다. 타입 이론 용어로 이 함수는 absurd와 동일한 타입을 가진다. 이름처럼 “프로그래머를 믿는 것은 불합리(absurd)하다”는 아이러니한 의미를 담고 있다. 만약 프로그래머의 주장이 실제로 거짓일 경우, 결과는 C와 C++에서 늘 마주하는 그 미정의 동작이다. 그러나 강연자가 흥미롭다고 강조하는 것은, DepC에서는 이 탈출구 사용 지점을 grep으로 코드베이스 전체에서 즉시 검색할 수 있다는 점이다. 암묵적으로 숨어 있는 위험이 아니라, 명시적이고 추적 가능한 위험이 된다는 것이다.
02:07 - 컴파일러에게 신뢰를 요청하는 탈출구(absurd) 사용 예제
증명 탐색 알고리즘의 내부 구조
컴파일러 내부에서 증명 탐색이 어떻게 이루어지는지를 강연자는 type_assigning이라는 함수를 중심으로 설명한다. 파서(parser)에서 넘어온 표현식을 분석하다가 배열 접근 연산자([])가 감지되면, 컴파일러는 인덱스가 경계 내에 있음을 증명해야 한다는 사실을 인지한다. 이때 증명 탐색 태스크(task)가 생성되며, 이 태스크는 다시 여러 개의 서브태스크(subtask)로 분기된다. 각 서브태스크는 서로 다른 **전술(tactic)**을 적용해 증명을 시도한다.
02:31 - type_assigning 함수 내부 - 배열 접근 감지 후 증명 탐색 태스크 생성 구조
강연자는 타입 이론적 관점에서 이 과정이 본질적으로 비결정적(nondeterministic)임을 인정한다. 즉, 증명이 반드시 발견된다는 보장이 없다. 이는 의존 타입 시스템을 실용적으로 구현하는 데 있어 공통적으로 직면하는 한계이기도 하다. 증명이 존재할 것으로 기대했지만 컴파일러가 찾지 못할 때, 개발자는 답답함을 느낀다. 이 문제를 해결하기 위해 강연자가 구현한 것이 바로 Perfetto 기반 트레이싱이다.
디버깅 도구 - Perfetto 트레이싱
증명 탐색에 실패했을 때, “왜 실패했는가”를 이해하는 것은 쉽지 않다. 컴파일러가 내부적으로 어떤 전술을 어떤 순서로 시도했고, 어디서 막혔는지를 알아야 하기 때문이다. 강연자는 이를 위해 Perfetto 트레이서(tracer)를 DepC에 연동하여, 증명 탐색 과정 전체를 시각적으로 기록할 수 있도록 구현했다. Perfetto는 구글이 개발한 오픈소스 시스템 프로파일링 및 트레이싱 도구로, 복잡한 비동기 이벤트 흐름을 타임라인 형태로 시각화하는 데 강점이 있다.
이 기능을 활성화하면 컴파일러가 시도한 모든 전술, 생성한 모든 서브태스크, 그리고 각 시도의 성공/실패 여부가 기록된다. 덕분에 개발자는 “이 증명은 왜 찾지 못했는가”에 대한 구체적이고 추적 가능한 답을 얻을 수 있다. 이는 단순한 오류 메시지를 넘어, 컴파일러의 추론 과정 자체를 투명하게 드러내는 접근이라는 점에서 의미가 있다.
03:13 - Perfetto 트레이서를 활용한 증명 탐색 실패 원인 분석 화면
마무리 - 핵심 정리
이 라이트닝 토크는 짧지만, 여러 층위의 아이디어를 압축적으로 전달한다. 핵심은 의존 타입 시스템이 C 언어의 가장 오래된 미정의 동작 원인 중 하나인 배열 경계 위반을 컴파일 타임에 정적으로 차단할 수 있다는 것이다. DepC는 이를 argc/argv 관계처럼 프로그래머에게 익숙한 패턴에서 출발하여, 컴파일러가 자동으로 증명을 탐색하는 방식으로 구현한다.
탈출구(absurd)의 존재는 실용성을 위한 현실적 타협이지만, 그조차 코드베이스에서 추적 가능하도록 설계되어 있다는 점이 중요하다. 그리고 증명 탐색이 실패할 때 Perfetto로 그 과정을 해부할 수 있다는 것은, 이 시스템이 단순한 연구 프로토타입을 넘어 실제 개발 워크플로를 고려하고 있음을 보여준다. 의존 타입이라는 다소 난해한 타입 이론의 개념이 실제 시스템 프로그래밍 언어에서 어떻게 구체화될 수 있는지를 보여주는 흥미로운 사례다.
📚 참고 자료 (강연 내용과 별개)
강연자가 언급한 **커리-하워드 대응(Curry-Howard Correspondence)**은 이 토크를 이해하는 데 핵심적인 배경 지식이다. 강연자 스스로 “직접 검색해보라”고 권한 만큼, 아래 개념들을 추가로 탐색하면 이 토크의 내용을 더 깊이 이해할 수 있다.
커리-하워드 대응은 1934년 Haskell Curry와 1969년 William Alvin Howard의 연구를 거쳐 정립된 원리로, 프로그래밍 언어의 타입 시스템과 논리학의 명제 체계 사이에 구조적 동형성이 존재함을 말한다. 이 대응 덕분에 “타입의 값을 찾는다”는 프로그래밍적 행위가 “명제를 증명한다”는 논리적 행위와 동일하게 취급될 수 있다. Coq, Agda, Idris, Lean 같은 언어들이 이 원리를 토대로 구축된 대표적인 의존 타입 언어들이다. DepC는 이러한 의존 타입의 개념을 C 언어 계열 시스템 프로그래밍 환경에 접목하려는 시도로 볼 수 있다.
Perfetto 트레이서에 대한 추가 정보는 https://perfetto.dev에서 확인할 수 있다. (본 리포트에서 직접 링크를 검증하지는 않았으므로 참고용으로만 활용하세요.)
📚 출처 및 참고
| 구분 | 내용 |
|---|---|
| 원본 영상 | Lightning Talk: Proof Searching in DepC - Raffaele Rossi - CppCon 2025 |
| 채널 | CppCon |
| 발표자 | Raffaele Rossi (Maven 테크 리드, DepC 기여자) |
| 컨퍼런스 | CppCon 2025 |
| 리포트 작성 | 2026-05-15 |
| 작성 방식 | YouTube 영상 STT 변환 후 에디팅 |
💬 본 리포트는 영상 내용을 바탕으로 재구성되었습니다. 정확한 내용은 원본 영상을 참조해 주세요.
Related Reports
- Lightning Talk - The Lifecycle of This CMake Lightning Talk - Yannic Staudt - CppCon 2025
- Lightning Talk - The Type Safe Builder Pattern for C++ - John Stracke - CppCon 2025
- Lightning Talk: When Weird Things Happen - Ruslan Arutyunyan - C++Now 2026
- Lightning Talk: Only Forward - Why Concurrency Works in C++