프로그램 검증을 위해 Lean 대신 Rocq를 선택하는 이유를 언어 기능, 추출, 생태계, 규제 수용성, AI 에이전트 관점에서 살펴본다.
특히 지금처럼 AI가 수학에서 거둔 성공이 널리 알려진 상황에서, 사람들은 왜 내가 과장된 열기에 휩쓸려 Lean으로 옮기지 않고 여전히 Rocq를 쓰는지 묻곤 한다. 이 글의 상당 부분은 최근 LangSec 기조연설에서 쓴, 도발적인 제목의 슬라이드에서 시작되었다. 제목은 “프로그램 검증에서 Rocq가 Lean보다 더 나은 이유”였다.
여기서 싸움을 시작하려는 것은 아니다. 나보다 더 성숙한 사람이라면, 아래의 모든 “더 낫다”를 마음속으로 “오늘날 내 작업에 더 잘 맞는다”로 바꾸어 읽어도 좋다. 시작하기 전 한 가지 단서가 더 있다. 이 글은 수학 형식화가 아니라 프로그램 검증에 관한 글이며, 수학 형식화에서는 Lean이 실제로 상당한 탄력을 얻고 있음을 기꺼이 인정한다.
Lean FRO의 Wojciech Różowski와 Joachim Breitner는 Lean에서 공귀납 술어를 지원하는 기능을 개발했다. 이 기능은 coinductive 명령으로 Lean 4.25에 포함되었다(구현). 이는 이중 시뮬레이션과 다른 공귀납 증명에 유용하지만, 실행 가능한 cofixpoint나 추출 가능한 프로그램을 제공하지는 않는다.
나는 실제로 실행할 수 있는 Type의 codata도 원한다. Rocq는 CoInductive와 CoFixpoint로 이를 직접 제공한다. Lean에는 Type에서 이에 대응하는 선언이 없으며, 대안은 일반 함수와 구조체 또는 라이브러리 인코딩을 사용한다.
Rocq 스타일 codata 선언에 가장 가까운 Lean 실험으로 내가 찾은 것은 Alex Keizer의 QPFTypes다. 이는 일반적인 codata를 위한 개념 증명 패키지다. codata 명령은 명세를 라이브러리 인코딩으로 바꾸고 소멸자, corecursor, 이중 시뮬레이션 원리를 생성한다. Rocq의 CoInductive와 달리 커널 선언은 아니다. 예제는 QPFTypes에 고정된 Lean 4.25.0 도구 체인을 사용한다(글 작성 당시 지원되는 최신 버전).
이것은 QPFTypes를 조롱하려는 말이 아니다. README에 바로 “개념 증명”이라고 쓰여 있다. 하지만 Rocq에서는 완전히 평범한 예제에서도 거친 부분이 빠르게 드러난다. 예를 들어 Rocq는 매개변수 없는 이 공귀납형을 직접 받아들인다.
CoInductive co_unit : Type :=
| co_unit_loop : co_unit.
codata CoUnit where
| loop : CoUnit
/--
error: Due to a bug, codatatype without any parameters don't quite
work yet. Please try adding parameters to your type
-/
이 경우는 구현 버그로 치부할 수 있지만, 다음 두 경우는 구조적이다. 상호 공귀납 선언은 Rocq에서는 일상적이지만 QPFTypes는 지원하지 않는다.
CoInductive tree (a : Type) : Type :=
| node : a -> forest a -> tree a
with forest (a : Type) : Type :=
| fnil : forest a
| fcons : tree a -> forest a -> forest a.
mutual
codata Tree α where
| node : α → Forest α → Tree α
codata Forest α where
| fnil : Forest α
| fcons : Tree α → Forest α → Forest α
end
/--
error: invalid mutual block: either all elements of the block must be
inductive/structure declarations, or they must all be definitions/
theorems/abbrevs
-/
인덱싱된 공귀납 패밀리 역시 Rocq의 일반적인 공귀납 조각에 속하지만 QPF 인코딩의 범위 밖이다. 이 예제에서 인덱스는 매 단계 전진하는 시계다. 같은 패턴은 프로토콜, 단계, 크기, 상태 기계에서도 나타난다.
CoInductive istream (a : Type) : nat -> Type :=
| icons : forall n, a -> istream a (S n) -> istream a n.
codata IStream α : Nat → Type where
| icons : α → IStream α (n + 1) → IStream α n
/--
error: Unexpected type; type will be automatically inferred. Note that
inductive families are not supported due to inherent limitations of QPFs
-/
내부적으로 QPFTypes는 Cofix 장치를 생성한다. codata 명령은 단순하고 비상호적이며 비인덱싱된 경우에 그 대부분을 숨기지만, 이 조각을 벗어나면 저수준 MvQPF.Cofix.corec 및 bisim API를 직접 호출해야 하거나 방법이 없다. Rocq에서는 위 예제들이 그저 선언일 뿐이다.
Rocq의 직접 지원도 고통이 없는 것은 아니다. guardedness 검사기와 씨름해 본 사람이라면 누구나 안다. 증명 측면에서 Rocq 사용자는 Paco나 Damien Pous의 coinduction 라이브러리 같은 성숙한 도구도 쓴다. 이들은 공귀납 술어와 관계에 도움이 되지만, 프로그램을 위한 CoFixpoint를 대체하지는 않는다.
네이티브 Rocq cofixpoint는 실제 지연 OCaml 값으로 추출된다. 예를 들어 내가 작업한 게임 트리 라이브러리에서 Rocq의 unfold_cotree 함수는 다음으로 추출된다.
type 'a cotree = 'a __cotree Lazy.t
and 'a __cotree =
| Conode of 'a * 'a cotree colist
(* other definitions ... *)
(** val unfold_cotree : ('a1 -> 'a1 colist) -> 'a1 -> 'a1 cotree **)
let rec unfold_cotree next init =
lazy (Conode (init, (comap (unfold_cotree next) (next init))))
QPFTypes에서는 대신 구성과 관찰이 일반적인 MvQPF.Cofix.corec 및 MvQPF.Cofix.dest 연산을 거친다. 프로그램은 위의 직접적인 지연 트리가 되지 않고 일반적인 Cofix 표현을 유지한다. 수학으로서는 괜찮지만, 내가 손으로 작성할 프로그램은 아니다.
QPFTypes를 직접 살펴보고 싶다면, BadCoinduction.lean에 이 절의 전체 실험이 들어 있다. 작동하는 Colist 및 Cotree 정의, 생성된 인터페이스 예제, 매개변수 없는·상호·인덱싱된 codata의 검사된 실패가 담겨 있다. 헤더에는 테스트를 다시 실행하는 데 필요한 정확한 QPFTypes 커밋과 명령이 기록되어 있다.
이쯤에서 Lean 프로그래머는 화면을 향해 외칠지도 모른다. 스트림을 쓰려고 QPFTypes를 꺼내는 사람은 없다고. 맞는 말이다. QPFTypes를 여기서 다루는 이유는 Rocq 스타일 codata 선언에 가장 가깝기 때문이다. 일상적인 Lean에서는 다른 여러 기법을 쓴다.
스트림에는 mathlib의 Stream'가 명백한 답이다. 이는 그저 Nat → α다. 위치 n을 요청하면 원소를 돌려준다. 실행 가능하며, mathlib는 extensionality, 이중 시뮬레이션, 공귀납 보조정리와 함께 corecursor도 제공하므로 이에 관해 증명하기 좋다. 하지만 꼬리가 또 다른 스트림인 지연 생성자는 아니다. 이는 스트림을 해결할 뿐, 임의의 상호 또는 인덱싱된 codata를 해결하지는 않는다.
또 다른 선택지는 명시적인 상태 기계다. 상태를 유지하고 단계 함수를 작성한 뒤 corecursor로 사용한다. Lean의 현재 Iter 인터페이스는 수열을 위해 이 패턴을 묶으며, 필요할 때 한 단계씩 계산한다. 반복자는 결국 값을 산출하거나 끝날 것이라는 Productive 증명을 가질 수 있고, Iter.repeat에는 이미 그것이 있다. 사용자 정의 반복자에서는 단계 인터페이스, 그 불변식, 그리고 어쩌면 생산성 증명을 제공해야 한다. 이는 작동하지만, 이제 상태 기계와 수열 사이의 배관 작업을 내가 직접 하고 있다. Rocq CoFixpoint는 재귀 호출의 guardedness를 검사하고 공귀납 값을 직접 준다.
Thunk는 지연성을 제공하지만 공귀납을 제공하지는 않는다. 컴파일된 Lean은 thunk가 강제될 때까지 지연시킨 후 결과를 캐시한다. 논리는 이를 Unit → α로 보므로, thunk를 포함하는 전함수 정의는 증명에서 계속 사용할 수 있지만 캐싱은 보이지 않는다. thunk는 재귀를 허용하지도, 재귀가 결국 생성자를 낸다는 점을 검사하지도 않는다. 추출된 Rocq cofixpoint는 재귀가 guardedness 검사기를 통과한 뒤에야 비슷한 런타임 지연성을 사용한다.
partial def는 무딘 도구다. 컴파일러는 재귀 본문을 실행하지만, 논리는 불투명한 상수만 얻는다. Lean은 여기서 종료성이나 생산성을 검사하지 않는다. 자연수의 thunk된 생성자도, 즉시 자기 자신을 영원히 호출하는 생성자도 받아들인다. unsafe def도 실행되지만, 정리에 안전한 선언은 이를 전혀 언급할 수 없다. Batteries의 MLList는 흔한 구성을 보여 준다. 비공개 unsafe 지연 구현, 불투명한 공개 인터페이스, 그리고 partial def로 작성된 fix, iterate 같은 생성자다. 이 생성자들은 관찰된 Rocq cofixpoint처럼 증명에서 전개할 수 없다. Lean에는 방정식을 유지하는 partial_fixpoint도 있지만, 이런 종류의 생성자와 thunk 재귀는 받아들이지 않는다.
QPFTypes는 그 불투명성을 피한다. corecursor와 이중 시뮬레이션 원리를 주기 때문이다. 그러나 그러면 다시 일반적인 Cofix 표현과 위에서 시험한 선언 제한으로 돌아간다.
왜 스트림 너머를 걱정하는가? 상호작용 트리 때문이다. Rocq의 상호작용 트리 라이브러리는 효과를 가지며 종료하지 않을 수도 있는 프로그램을 공귀납 트리로 표현한다. 이를 이용해 프로그램을 작성하고, 그 프로그램을 해석하고 추출하며, 보통 약한 이중 시뮬레이션까지 고려해 같은 트리에 관한 방정식을 증명할 수 있다. Stream'과 Iter는 수열만 주며 효과에 필요한 분기 연속을 주지 않는다. Thunk와 partial def로 손수 작성한 효과 트리를 실행할 수는 있겠지만, 그러면 재귀 생성자가 증명에 대해 불투명해진다. Lean에서 이 모든 것을 얻으려면 codata의 라이브러리 인코딩이 필요하다.
MIT PLV의 lean4-itree는 Mathlib의 PFunctor.M 최종 coalgebra를 사용해 상호작용 트리에 이를 제공한다. 더 새로운 PolyFun은 핸들러, 재귀 절차, 트레이스, 강하고 약한 이중 시뮬레이션, 모나드 및 반복 법칙 증명을 추가한다. 이 트리로 계산하고 Lean에서 그에 관해 증명할 수 있다. 그래도 라이브러리로 인코딩된 M-타입이다. Lean에는 여기서 네이티브 codata 선언이 없으며, 계산은 Rocq가 추출하는 직접적인 지연 프로그램을 만들지 않고 일반적인 표현을 유지한다.
HITrees는 이 문제를 우회하는 방법이 아니다. 저자들은 ITrees가 사용하는 공귀납 Delay-모나드 접근을 검토하지만, Lean에 네이티브 공귀납형이 없어서 이를 배제한다. 그들의 트리는 대신 귀납적이며, 비종료는 고차 재귀 효과가 된다. 재귀 계산은 더 이상 관찰하고 전개할 수 있는 무한 트리가 아니다. 핸들러가 그 효과를 해석할 때에만 재귀에 의미가 부여된다. 모나드 해석은 이를 실행할 수 있고, 증명은 상태 기계 해석을 거쳐 진행할 수 있지만, HITree 등식 이론은 일반적인 재귀 전개 방정식을 제공하지 않는다. 작동은 한다. 하지만 비종료를 트리에서 해석기로 옮기며, 나는 guarded Rocq cofixpoint를 작성하는 것보다 이것이 더 불편하다고 느낀다.
Lean에서는 이들 중 하나를 포기하거나 일반적인 장치 위에 다시 구축해야 한다. Rocq에서는 codata를 선언하고, guarded 생성자를 작성하고, 관찰로 이에 관해 추론하고, 직접적인 지연 코드를 추출할 수 있다. 이것이 내가 공귀납에서 원하는 것이다.
Meven Lennon-Bertrand가 이것을 내게 알려 주었고, 나는 아래 예제를 확장했다. Lean은 많은 중첩 귀납 정의를 받아들이지만, Rocq가 받아들이는 일부 정의는 검사기가 거부한다. 나는 증명 진주 A Rose Tree Is Blooming를 작성하면서 이를 만났고, 이 증명은 Rocq의 이 부분에 의존한다. Lean으로 작성했다면 훨씬 더 지저분했을 것이다. 장미 트리 예제는 이 글에 넣기에는 너무 크므로, 여기서는 JSON 스키마로 같은 문제를 보이겠다.
JSON 스키마 언어가 있고 검증에 관한 일반적인 사항을 증명하고 싶다고 하자. 필드 이름이 맞아떨어지고, 스키마에서 필드를 제거해도 안전하며, 접두사를 검증할 수 있다는 것들이다. 검증된 시스템을 만든다면 평범한 일이다. JSON과 스키마 정의는 어느 언어에서도 문제가 없다.
Inductive json : Type :=
| jnull : json
| jstr : string -> json
| jnum : nat -> json
| jarr : list json -> json
| jobj : list (string * json) -> json.
Inductive schema : Type :=
| sany : schema
| sstr : schema
| snum : schema
| sarr : schema -> schema
| sobj : list (string * schema) -> schema.
inductive JSON where
| null : JSON
| str : String → JSON
| num : Nat → JSON
| arr : List JSON → JSON
| obj : List (String × JSON) → JSON
inductive Schema where
| any : Schema
| strS : Schema
| numS : Schema
| arrS : Schema → Schema
| objS : List (String × Schema) → Schema
흥미로운 부분은 검증 관계다. { "name": string, "age": number } 같은 객체 스키마는 필드 이름이 일치하고 각 값이 대응하는 하위 스키마에 대해 검증되는지 쌍별로 확인하여 { "name": "Alice", "age": 30 } 객체를 검증해야 한다. Rocq는 이 모든 것을 하나의 Forall2 도출에 담을 수 있다.
Inductive valid : schema -> json -> Prop :=
| valid_any : forall j, valid sany j
| valid_str : forall s, valid sstr (jstr s)
| valid_num : forall n, valid snum (jnum n)
| valid_arr : forall elem_schema elems,
Forall (fun j => valid elem_schema j) elems ->
valid (sarr elem_schema) (jarr elems)
| valid_obj : forall schema_fields json_fields,
Forall2
(fun (sf : string * schema) (jf : string * json) =>
fst sf = fst jf /\ valid (snd sf) (snd jf))
schema_fields json_fields ->
valid (sobj schema_fields) (jobj json_fields).
프로젝션은 의도적이다. Rocq 9.0은 재귀 발생 주변의 동등한 튜플 패턴 람다를 엄격한 양성이 아니라며 거부한다. 구문 검사기는 그 패턴 매치를 꿰뚫어 보지 못한다. 위의 프로젝션 기반 선언은 컴파일된다.
Lean 4.32.1은 대응하는 객체 생성자를 거부한다.
inductive ValidCombined : Schema → JSON → Prop where
| obj :
Forall₂
(fun (sf : String × Schema) (jf : String × JSON) =>
sf.1 = jf.1 ∧ ValidCombined sf.2 jf.2)
schemaFields jsonFields →
ValidCombined (.objS schemaFields) (.obj jsonFields)
error: (kernel) invalid nested inductive datatype 'And',
nested inductive datatypes parameters cannot contain local variables.
Lean은 인접한 여러 형태를 받아들인다. Forall₂ ParRed, And와 Exists를 통한 직접 재귀, 그리고 Forall₂ (fun sf jf => Valid sf.2 jf.2)다. 거부된 선언에서 재귀 발생은 Forall₂와 And를 모두 통과하며, 커널은 내부 And를 보고한다. 다른 경우인 Forall₂ (Eval env)는 관계 매개변수가 생성자 지역 env를 포획하므로 Forall₂에서 실패한다.
Lean은 결합 관계를 두 Forall₂ 도출로 나누어 목록 구조를 유지할 수 있다.
inductive Valid : Schema → JSON → Prop where
| obj :
Forall₂
(fun (sf : String × Schema) (jf : String × JSON) =>
sf.1 = jf.1)
schemaFields jsonFields →
Forall₂
(fun (sf : String × Schema) (jf : String × JSON) =>
Valid sf.2 jf.2)
schemaFields jsonFields →
Valid (.objS schemaFields) (.obj jsonFields)
인덱스나 별도의 길이 증명은 필요 없다. 머리를 제거하는 일은 구조적으로 남아 있지만, Lean은 두 도출을 모두 분해해야 한다.
Lemma Forall2_tail :
forall (A B : Type) (R : A -> B -> Prop)
(a : A) (b : B) xs ys,
Forall2 R (a :: xs) (b :: ys) ->
Forall2 R xs ys.
Proof.
intros. inversion H; assumption.
Qed.
theorem Valid.dropHead
(hv : Valid (.objS ((k, s) :: schemaFields))
(.obj ((k', j) :: jsonFields))) :
Valid (.objS schemaFields) (.obj jsonFields) := by
cases hv with
| obj hnames hvalues =>
cases hnames
cases hvalues
exact .obj
‹Forall₂ _ schemaFields jsonFields›
‹Forall₂ _ schemaFields jsonFields›
관계를 나누면 각 이름 동등성과 재귀 검증을 짝짓는 하나의 증명 객체를 잃는다. 상호 ValidFields 관계로 그 짝짓기를 복구할 수 있지만, 그러면 Lean의 induction 전술은 상호 귀납형을 지원하지 않고 생성된 recursor는 모든 관계에 대한 motive를 받는다. 사용자 정의 귀납 정리는 그 설정을 숨길 수 있다. Rocq는 표준 Forall2 표현을 유지하며, 상호 정의가 필요할 때 Scheme으로 결합 원리를 생성할 수 있다.
Lean도 인덱스 기반 인코딩 없이 같은 명제를 표현할 수 있지만, 선언을 재배열하고 더 많은 증명 장치를 만들어야 한다. list Term을 포함하는 Term 같은 중첩 데이터에 대해서는 어느 시스템도 원소별 귀납 원리를 자동으로 제공하지 않는다. 둘 다 목록 원소에 관한 가설을 위한 더 강한 recursor가 필요하다(Meven은 Rocq 9.2가 이를 고친다고도 알려 주었다. 자세한 내용은 각주 참조: 1).
전체 비교를 직접 실행할 수 있다. NestedPain.v는 Rocq 9.0.0 쪽이고, NestedPain.lean은 Lean 4.32.1 쪽이다. Lean 파일은 예상되는 실패를 #guard_msgs로 감싸므로, 오류가 시험되지 않은 주석으로 남는 대신 컴파일 중 검사된다.
결국 나는 이 정의들이 실행할 수 있는 프로그램이 되기를 원한다.
Lean은 추출에 대해 분명한 입장을 취한다. 표준 도구 체인은 자체 런타임을 통해 컴파일한다. 물론 Lean 라이브러리를 작성하고 런타임 설계가 요구에 맞는다면 이는 진정한 장점이다. 그리고 성능 면에서 Lean의 표준 도구 체인은 확실히 인정받아야 한다. Kim Morrison의 검증된 lean-zip은 순수 Rust miniz_oxide보다도 더 빠르게 압축할 수 있다! 인상적이다. 하지만 성능이 추출의 전부는 아니다. 나는 생성된 코드를 읽을 수 있는지, 대상 언어를 고를 수 있는지, 검증된 파이프라인에 넣을 수 있는지도 신경 쓴다.
Lean은 대체 추출 백엔드 메뉴를 제공하지 않으며, 갖춘 컴파일 파이프라인도 종단 간 정확성 증명을 제공하지 않는다(그래서 Kiran Gopinathan이 발견한 사례 같은 드문 런타임 버그가 있다). 또한 내 생각에는 읽기 쉽지 않다(그렇게 설계된 것이 아니므로 당연하다! 생성된 코드는 런타임에 매우 특화되어 있다).
반대로 Rocq는 정의에서 실행 가능한 프로그램으로 가는 여러 경로를 제공하며, 각각 TCB, 가독성 등에서 서로 다른 절충을 가진다.
아마 이 경로 중 하나는 맞을 것이다.
생태계는 내가 가볍게 대체할 수 없는 부분이다. 아래 기반 시설 대부분은 Rocq로 작성되었고, 몇몇 항목은 확립된 Rocq 백엔드나 구성 요소를 가진 외부 도구다.
추상화:
프로그램 검증 프레임워크:
Rocq 백엔드 또는 구성 요소를 가진 검증 도구:
실제 언어를 위한 형식 의미론과 검증된 컴파일러:
번역을 통한 경량 검증:
프로그램 합성:
검증된 어휘 분석과 파싱:
이 목록을 훑고 “이 중 어느 것도 큰일은 아니야. 필요한 부분을 주말 동안 AI로 Lean에 포팅하면 되지.”라고 생각할 수도 있다. 그럴 수 있다. 하지만 한 절만 더 그 생각을 붙들어 두자.
이 프로젝트들 중 일부는 활발히 유지보수되지 않는다는 점은 인정해야겠다. 그래도 내 경험상, 대개 에이전트 하나를 투입하면 꽤 쉽게 다시 빌드하고 실행되게 할 수 있다.
나는 도구를 인증 절차에 통과시켜 본 직접 경험이 없으며, 규제 수용성 전문가도 아니다. 이 점은 Meven에게서 나왔다. 그는 이것이 나보다 유럽 동료들에게 더 중요할 수 있다고 지적했다.
ANSSI는 Common Criteria 평가에서 Rocq 사용 기준을 발표했다. CompCert 프로젝트는 2026년에 Airbus의 지침 아래 AbsInt가 수행한 작업으로, 컴파일러가 ATR 42/72 항공기의 MFC_NG 컴퓨터에 대해 성공적으로 적격 판정을 받았다고 보고한다.
두 환경 중 어느 쪽이든 Lean 포트에 무엇이 요구될지는 내가 말할 수 없다. 깔끔한 주말 포트조차 그 이력을 자동으로 물려받지는 않는다. 수용될지는 이 절차를 잘 아는 사람들이 답할 문제다.
이것이 실제로 가장 자주 받는 질문이다. 모든 과장은 AI 에이전트가 Lean을 작성하게 만드는 데 집중되어 있다는 것을 안다. 하지만 에이전트는 Rocq를 작성하는 데도 아주 능하다.
“AI는 인기 있는 언어만 안다”는 주장은 유효 기간이 짧으며, 내가 증명 보조기를 바꿀 이유도 아니다.
Lean은 진지한 프로그램 검증 작업을 하고 있다(mvcgen과 Velvet을 보라!). 하지만 내 작업을 그곳으로 옮기려면 여전히 정의를 재구성하고, 내가 이미 의존하는 추출 파이프라인, 라이브러리, 제도적 이력을 대체해야 한다. 내가 실제로 하는 작업을 고려하면, 오늘날 Rocq가 나에게 더 잘 맞는다.
All 술어와 그 정리가 등록되면 중첩 인수에 대한 귀납 가설을 생성한다. 표준 라이브러리는 아무것도 등록하지 않으므로, 여전히 한 줄은 직접 작성해야 한다. Term 선언 전에 Scheme All for list.를 넣으면 생성되는 Term_ind와 Term_rect는 app 경우에 list_all Term P l 가설을 얻고, 본문은 list_all_forall을 호출한다. 이것은 내가 손으로 작성한 Term_rect_strong과 정확히 같으므로, ParRed_refl은 평범한 induction term으로 진행된다. 중첩 관계에도 작동한다. Scheme All for Forall2. 뒤에는 ParRed_ind가 Forall2 ParRed args args' 전제에 대한 귀납 가설을 준다. Scheme All 줄이 없으면 이전의 약한 원리와 함께 이를 추가하라는 [register-all] 경고가 나온다. Lean에는 여전히 더 강한 recursor가 필요하다.↩︎