프로그램 검증에서 Rocq가 Lean보다 나은 이유

수학 형식화에서 Lean의 성장세는 뚜렷하지만, 실행 가능한 프로그램 검증에는 네이티브 공귀납과 다양한 추출 경로, 축적된 검증 생태계를 갖춘 Rocq가 더 잘 맞음 Rocq는 CoInductive와 CoFixpoint로 공데이터를 선언하고 guardedness를 검사한 뒤 지연 실행 코드로 추출하지만, Lean에서는 라이브러리 인코딩·이터레이터·Thunk·partial def 중 하나를 선택해야 함 Lean의 중첩 귀납 타입 검사기는 Rocq가 허용하는 일부 검증 관계를 거부해, JSON 스키마 사례에서는 하나의 Forall₂ 증명을 여러 관계로 분리하고 별도의 귀납 원리를 마련해야 함 Rocq는 OCaml·Haskell·Rust·C++·WebAssembly 등의 프로그램 추출 경로와 Iris·CompCert·Interaction Trees 같은 검증 기반을 제공해 실제 게임의 검증된 로직을 실행 코드로 연결할 수 있음 AI 에이전트도 문서와 사례가 있으면 Rocq 코드를 작성할 수 있으며, Lean으로 전환하려면 정의뿐 아니라 추출 파이프라인·라이브러리·규제 및 제도적 이력까지 대체해야 하므로 현재 작업에서는 실익이 부족함 프로그램 검증을 기준으로 한 비교 비교 대상은 수학 형식화가 아니라 프로그램 검증이며, 수학 분야에서는 Lean이 실제 성장 동력을 갖고 있음 “더 낫다”는 절대적인 우열이 아니라 현재 수행하는 작업에 Rocq가 더 잘 맞는다는 뜻임 AI의 수학 분야 성과와 Lean에 대한 관심이 커지면서 Rocq를 계속 사용하는 이유를 자주 질문받았고, 논지는 LangSec 기조연설의 슬라이드에서 출발함 네이티브 공귀납 타입과 cofixpoint Lean의 coinductive가 제공하는 범위 Lean FRO의 Wojciech Różowski와 Joachim Breitner가 개발한 공귀납 술어 지원은 Lean 4.25의 coinductive 명령에 포함됨 이 기능은 bisimulation과 공귀납 증명에는 유용하지만, Type의 실행 가능한 cofixpoint나 추출 가능한 프로그램을 제공하지 않음 Rocq의 CoInductive와 CoFixpoint는 실행 가능한 공데이터(codata) 를 Type에 직접 제공함 Lean에는 이에 대응하는 커널 선언이 없어 일반 함수·구조체 또는 라이브러리 인코딩을 사용해야 함 QPFTypes의 선언 제약 Alex Keizer의 QPFTypes는 일반 공데이터를 위...