はじめに
証明を書き終えたとき、プログラムはもう出来上がっている ── そんな言語があります。
ふつうの開発では、プログラムを書いてから、テストで正しさを確かめます。テストは、試した場合についてしか、正しさを保証しません。
この順序を逆さまにした世界があります。
先に「この計算は正しい」という数学の証明を書く。
すると、その証明の中から、動くプログラムを Rocq の処理系（Rocq という言語を実際に動かすコンピュータ上のプログラム本体）が取り出してくれる
── 取り出されたプログラムの計算内容は、Rocq の上で性質の証明と検査を済ませたものです。
テストで後から確かめるのではなく、正しさの検査が先に済んでいます。
【中上級者向け発展解説】「処理系が取り出す」の内訳 ── カーネルと Extraction
本文では「Rocq の処理系」と一語で呼びますが、正確には、この中で役割の違う２つの部品が働いています。
検査を担うのは、カーネルと呼ばれる小さな中核です。
証明が正しいかどうかの判定は、意図的に小さく作られたこの部品に集中させてあります。
信頼しなければならない範囲を、できるだけ狭く保つための設計です。
取り出しを担うのは、Extraction という別の仕組みです。
カーネルの検査を通った定義を受け取り、OCaml などのコードへ変換します。
つまり本文の一文は、正確には、「カーネルが検査を済ませ、Extraction がコードを生成する」という分担 で動いています。
なお、Extraction による変換そのものはカーネルの外側の処理であり、変換の正しさをどこまで形式的に保証するかは、それ自体が研究の主題です。
本記事の範囲では、 「検査と取り出しは、別の部品の仕事」 とだけ押さえておけば充分です。
この仕組みを40年磨き上げてきた言語が、Rocq（ロック） です。
Rocq は、1980年代にフランスの国立研究所 INRIA で生まれた、定理証明の世界では老舗の言語 です。
長らく Coq（コック） という名前で知られ、2025年に Rocq へ改名されました。
本記事では現在の名前 Rocq で呼び、歴史の話では旧名 Coq も使います。
そして、この言語には 実務の成果が実在します。
- 検証済みのCコンパイラ CompCert
- Google の暗号ライブラリに採用された検証済みコードを生み出した Fiat-Crypto
どちらも、「証明からプログラムを取り出す」という、この言語の最大の個性の上に建っています。
本記事は、Rocq も、定理証明をこれまで学んだことのない Python エンジニアの方々に向けて、前提知識ゼロからこの言語の個性と成果を説明する記事です。
この記事の全体像 ── 順路と結論を最初に
結論を先に述べます。
Rocq の最大の個性は、「証明からプログラムを取り出せる」ことです。
「条件を満たす値が存在する」という証明を、その値を実際に組み立てて見せる形で書くと、組み立ての手順だけを Rocq の処理系が抜き出して、OCaml などの言語の動くコードに変換してくれます。
正しさの議論は消え、検証済みの計算手順だけが残る
── この仕組みは、抽出（ちゅうしゅつ） と呼ばれます。
そして、この個性は絵空事ではありません。
抽出の仕組みの上に、検証済み C コンパイラ CompCert と、検証済み暗号コードの Fiat-Crypto という、実務で使われる成果が建ちました。
ビジネス事例がほぼ無い言語を紹介した 前回の記事（Cubical Agda） とは対照的に、今回は事例が実在する側の話 です。
実例を見てみましょう。
- 関数を定義し、
- 性質を証明し、
- 性質を満たす実例を構成する手順を実行可能なコードとして取り出す
── 最小の実演です。
Rocq のコードを初めてご覧になる方のために、コードの読み方の解説を書き添えさせていただきます。
（本格的な全行解説は、この記事の第２部で行います）。
Definition double (n : nat) : nat := n + n.
Theorem double_ok : forall n : nat, double n = n + n.
Proof.
intros n. reflexivity.
Qed.
Require Extraction.
Extraction Language OCaml.
Extraction double.
最初に、コード中に登場する各語彙の区別を伝えます。
このコードのうち、double、double_ok、n の３つは、プログラマ（筆者）が自分の好きな名前を任意に付けた箇所 です。別の名前に変えてもコードは同じように動きます。
それ以外の語は、予約語 か、タクティク や ライブラリの名前 で、どれがどれかは読みながら示します。
タクティク について補足します。
タクティク とは、「この方針で証明を組み立てよ」 と Rocqの処理系 に与える 指示の言葉 です。
証明そのものを一字一句、定理証明エンジニア（人間）が手で書く代わりに、短い指示を並べて与えると、Rocqの処理系がその指示に従って証明を組み立て、正しさを確かめていってくれます。
上記のコードでは、intros n と reflexivity の ２語 が、タクティク に該当します。
最初の行が、関数の定義です。 double は、自然数（nat）を受け取って n + n を返す、ただの関数です。
続く４行が、性質の証明です。
Theorem の行 は、「 double_ok という名前で、『すべての自然数 $n$ について、double n は $n + n$ と等しい』という主張をこれから証明する」という 宣言 です。
Proof. と Qed. に挟まれた２語 ── intros n（任意の $n$ を取れ）と reflexivity（左右を計算して、同じになることを確かめよ）── が、Rocqの処理系 に与える指示（ タクティク と呼ばれます）です。
Rocqの処理系はこの指示に従って検査を行います。
最後の３行が、取り出しの命令です。
抽出の道具を読み込み、出力先の言語を OCaml に指定し、double を取り出します。
結果として、次のコードが出力されます（本記事の検証環境での、実機の出力そのままです）。
(** val double : nat -> nat **)
let double n =
add n n
OCaml についてご存知なくても、この記事をお読みいただく上は支障ありません。
上記の出力結果（OCamlのコード）は、Pythonでいえば def double(n): return n + n に相当する、ただの関数定義です。
注目すべきは、証明の過程が、出力に現れないことです。
double_ok の証明 ── Proof. から Qed. までの中身 ── は、取り出されたコードのどこにもありません。
正しさの議論は Rocq の中で検査を終えて消え、計算の手順だけが、OCamlの関数として出力されました。
「証明を書き終えたとき、プログラムはもう出来上がっている」という先ほどの文は、この状況を説明した文です。
以上をまとめると以下のようになります。
本記事では、定理証明の実務で行われている一般的な事例 と 筆者個人の着想やアイディア を区別できるように記載します。
想定読者
- Python は書けるが、定理証明・形式検証の言語（Rocq、Lean 4、Agda など）は学んだことがない方
- テストでは届かない正しさの保証に、関心か疑問を持っている方
- 検証済みコンパイラや検証済み暗号のニュースを聞いて、「どうやって作るのか」が気になっていた方
数学の予備知識は仮定しません。本文中の専門用語は、登場する前にすべて日常の言葉で組み立てます。
この記事を読む価値
- Rocq とは何か、旧名 Coq との関係、そして2025年の改名までを、歴史の流れごと説明できるようになる
- 「証明からプログラムを取り出す」という最大の個性を、原理（構成的証明）から仕組み（抽出）まで理解できるようになる
- タクティクという証明の書き方を、コードを１行ずつ読みながら体験できる
- 検証済み C コンパイラ CompCert と、検証済み暗号の Fiat-Crypto という実務の成果を、出典つきで知ることができる
- Lean 4・Agda・λProlog という近縁の言語たちと Rocq の役割の違いが、一枚の地図として頭に入る
- 日本語の書籍を含む、知識ゼロからの学習の道筋が分かる
TL;DR
（この節の専門用語は、いずれも本文で説明します）
- Rocq は、1980年代に INRIA で生まれた定理証明の老舗言語である。長年 Coq の名で知られ、2025年に Rocq へ改名された
- 最大の個性は抽出 ── 「条件を満たす値が存在する」ことを、その値を実際に組み立てて示す証明（構成的証明）から、組み立て部分だけを OCaml などの動くコードとして Rocq の処理系が取り出せる
- 取り出されたコードの計算内容は、Rocq の上で性質の証明と検査を済ませたものである。テストで後から確かめるのではなく、正しさの検査が先にある
- この仕組みの上に、検証済み C コンパイラ CompCert（商用利用あり）と、Google の暗号ライブラリに採用された Fiat-Crypto という実務の成果が実在する
- 証明はタクティク（証明の組み立てを Rocq の処理系に指示する命令の言葉）で書く。証明を関数として手で直接書く Agda とは、ここが対照的である
- 数学の形式化でも、四色定理や奇数位数定理という金字塔の実績を持つ
- Lean 4 とは近縁で、役割の分業がある ── 数学ライブラリの広さは Lean 4、証明からのプログラム抽出の道具立てと実績は Rocq
- 学習資産は厚く、日本語の書籍も実在する（Agda には無かった、この言語の強みのひとつ）
筆者のこれまでの記事について
本記事は単独で読めるように書いてあります。この節は、筆者が書いてきた関連記事の地図です（読み飛ばして構いません）。
筆者はこれまで、「数学の証明をコンピュータが検査する」という世界の言語たちを、Python エンジニア向けにひとつずつ紹介してきました。
-
Lean 4 とは何か ── 定理証明の二強のもう一角。AI が数学オリンピックに挑む舞台裏と、業務要件の検証への応用を書きました
-
Cubical Agda とは何か ── ビジネス事例がほぼ無いのに注目される研究言語の話です。本記事は、この記事と対になる「事例が実在する側」の一本です
-
λProlog とは何か ── 本記事の主役 Rocq の内側で働く、論理プログラミング言語の話です。第4部で再会します
-
F* とは何か ── 型に条件を書き込める言語（篩型）と、その業務応用の話です
- HoTT 連載（第１回）・HoTT 連載（第２回） ── 「複数の等しさ」の数学の連載です
まず、Rocq とはどんな言語か
Rocq を一言でまとめると、数学の証明をコンピュータの上で書き、Rocq の処理系に検査させ、さらにその証明からプログラムを取り出せる言語 です。
40年の歴史 ── Coq から Rocq へ
この言語の歴史は、定理証明の世界でも指折りの長さです。
起点は1984年のフランスです。国立研究所 INRIA で、論理学者ティエリー・コカンとジェラール・ユエが、証明とプログラムを同じ土台で扱う理論（後述します）の最初の実装を始めました。
1989年末、このシステムは Coq と命名されました。
これ以後、Coq は、大学と研究機関を中心に育てられてきました。
旧名の Coq はフランス語で 雄鶏 を意味します。
公式サイトの説明によれば、土台の理論（Calculus of Constructions、略してCoC） と、生みの親のひとりコカン（Coquand）の名前への参照 であり、フランスの国の象徴である雄鶏への敬意 も込めた命名であったとのことです。
そして2023年10月に改名が予告され、2025年3月のバージョン9.0のリリースをもって、名前は正式にRocq となりました。
新しい名前 は、この言語が生まれた研究所の所在地 Rocquencourt（ロカンクール）に敬意を表したもの です。
あわせて、力の象徴である伝説の巨鳥ロック（Roc） と、岩の堅牢さの連想 も込められています。
名前は、利用者コミュニティへの調査を経て、開発のコアチームが選びました。
では、改名で中身は変わったのでしょうか。
言語そのものは、これまでと同じものです。
バージョン9.0は旧 Coq 8.20 と互換で、既存の資産は互換の仕組みでそのまま使い続けることが可能です。
この互換性は、本記事でも確認済みです。
本記事のコードは、旧 Coq と改名後の Rocq 9.0 系の両方で、無修正のまま動きます（末尾の検証環境を参照）。
コマンドやライブラリの名称は変更されています。
コマンド群が rocq という１つの入口に統合され、標準ライブラリの名前空間も Coq から Stdlib に改められました。
なお、過去40年間、世界中で刊行された旧Coqに関する教科書や論文・ライブラリは、旧名Coq のまま流通しています。
証明は、タクティクで書く
Rocq の 証明の書き方 には、はっきりした流儀があります。タクティク です。
タクティク とは、「この方針で証明を組み立てよ」と Rocq の処理系に指示する、命令の言葉です。
証明を一字一句、定理証明エンジニア（人間）がみずからで書くのではなく、Rocqに対する指示（命令）を与えると、Rocqの処理系が証明の本体を組み立てていってくれます。
将棋の指し手のように、一手ずつ盤面（証明の残り課題）を進めていく感覚です。
このスタイルは、Lean 4 と共通です。
他方で、前回公開した記事で取り上げた Agda は、タクティク に頼らずに、定理証明エンジニアが、証明を関数として手で書いていくスタイルを採用しています。
定理証明の言語たちの、住み分け
筆者がこれまで取り上げてきた言語と並べると、Rocqの立ち位置 が見えてきます。
-
F* ：SMT ソルバという自動証明の火力を活用した、ソフトウェア検証（セキュリティ分野の実績）
-
Lean 4 ：数学ライブラリ Mathlib の蓄積を土台にした、数学の形式化と、業務検証への応用
-
Agda ：依存型プログラミングそのものを、混ぜ物なしで学び、試すための研究言語
-
Idris 2 ：依存型を日常のプログラミングに使うことを目指した、実務寄りの言語
- Rocq ：証明からプログラムを取り出す仕組みを核に、検証済みソフトウェアを生み出してきた老舗
この「取り出す」とは何なのか。次の第1部が、本記事の心臓部です。
第１部 ── 最大の個性:「証明からプログラムを取り出す」とは何か
「存在する」の、２つの言い方
土台の考え方を、具体例から組み立てます。
「 $1000$ より大きい素数は、存在する」という主張を、証明したいとします。
１つ目の方法 は、条件を満たす値を、実際に差し出す ことです。
「 $1009$ がそうです。$31$ までの素数のどれでも割り切れません
── 約数があるなら、小さいほうの約数は $1009$ の平方根（約 $31.8$ ）以下のはずなので、そこまで確かめれば十分です」。
この証明からは、主張が正しいという結論だけでなく、具体的な値（ $1009$ ）と、その確かめ方 まで手に入ります。
２つ目の方法 は、無いと仮定して、矛盾を導く ことです。
「 $1000$ より大きい素数が１つも無いと仮定すると、おかしなことになる。だから、有るはずだ」
この証明でも、主張は正しいと分かりますが、条件を満たす値は、１つも手に入りません。
数学では、どちらも証明として成立します。
Rocq で証明からプログラムを取り出すときに効くのが、１つ目の方法です。
「存在する」と言うためには、条件を満たす値を実際に組み立てて見せる 。
このスタイル（流儀）は、構成的証明 と呼ばれます。
証明の中に、プログラムが埋まっている
この流儀を選ぶと、面白いことが起こります。
「すべての入力 $n$ に対して、条件を満たす出力が存在する」という定理を、この流儀で証明したとします。
すると、その証明の中には、入力 $n$ から、条件を満たす出力の値を実際に組み立てる手順 が埋まっています。
手順とは、つまり（プログラミング言語の）実装プログラムです。
命題を型として、証明をその型の値として捉える。
すると、証明とプログラムのあいだに対応関係が浮かび上がります。
この 対応関係には、名前が付いています。
「カリー=ハワード対応」 という名前です。
Rocq は、この対応関係を、言語の設計の中心に置く処理系です。
抽出 ── 正しさの議論を消し、手順だけを残す
ここからが、Rocq の能力が本領発揮される見せ場となる部分です。
証明 の中には、２種類の材料が混ざって います。
計算の手順（答えの組み立て方）と、正しさの議論（その組み立てが条件を満たす理由）です。
プログラムとして動かしたいのは、手順のほうだけ です。
正しさをめぐる議論（証明過程） は、検査（証明）が済んだ後、証明された手順を実行するためのプログラミングコードを記述する際には、不要な情報です。
Rocq には、この選り分けを処理系が行う仕組みがあります。
証明済みの定義を渡すと、正しさの議論を消し、計算の手順だけを OCaml や Haskell のコードとして書き出してくれる ── これが抽出です。
出てきたコードは、ふつうの OCaml のプログラムとしてコンパイルして実行可能です。
そして、そのコードが満たすべき性質は、取り出す前に、Rocq の上で証明済み です。
テストで後から確かめるのではなく、正しいかどうかの証明が先に完了している
── 冒頭の「順序が逆さまの世界」の姿が、これです。
なぜ、OCaml言語として取り出すのか
取り出す先の言語として、OCaml がよく使われるのはなぜでしょうか。
理由は３つあります。
第１に、OCamlはRocqにとって、身内の言語だからです。
OCaml は、Rocq と同じフランスの INRIA で育った関数型言語で、Rocq の処理系そのものが OCaml で書かれています。
自分自身を実装してくれている言語を、抽出した計算手順を表現する実装コード言語として選択することは、自然で理にかなっています。
第２に、型の扱いの厳しさが近いからです。
Rocqは、型が合わないコードを一切通しません。
OCaml も同じで、実行する前の検査で、型の食い違いをすべて弾きます。
（強い型検査と呼ばれ、こうした性質を持つML系という言語族の一員です）。
第３に、OCaml が産業界で実際に採用されている言語だからです。
代表例は金融業界です。
─
米国の大手トレーディング会社ジェーン・ストリートは、取引システムの開発言語として OCaml を全面的に採用しています。
ブロックチェーンの Tezos も、中核部分はOCamlで実装されています。
型の堅牢さと実行速度を両立する言語として、OCamlは、誤りが重大な損失に直結する領域で採用されてきました。
証明から取り出したコードは、そのまま産業用途で稼働させられる言語で表現されている
抽出が机上の理論で終わらない理由のひとつです。
なお、計算手順の取り出し先の言語としては、Haskellなど も候補に挙がります。
本記事では、Rocqの公式ドキュメントが筆頭に挙げる OCamlで記事を書いていきます。
取り出し先は、OCaml だけではありません
取り出し先の言語を変えるのは、１行の書き換えだけ です。
全体像の実演で使ったコードのうち、Extraction Language OCaml. の行を書き換えます。
Require Extraction.
Extraction Language Haskell.
Extraction double.
書き換えたのは、真ん中の行の OCaml を Haskell にした一点だけです。
他の行 ── double の定義も、double_ok の証明も ── は、一字も変えていません。出力は次のようになります。
double :: Nat -> Nat
double n =
add n n
先ほどの OCaml の出力と並べてみます。
(** val double : nat -> nat **)
let double n =
add n n
同じ証明から、２つの言語の実装コードが取り出されました。
型の書き方（:: と val）や関数定義の記法が、それぞれの言語の作法に合わせて変わっているだけで、計算の中身は同一です。
取り出し先として指定できる言語は、OCaml と Haskell のほかに、Scheme と JSON があります。
Scheme を指定すると、次のように括弧の並んだ Lisp系の記法 で出力されます。
(define double (lambda (n) (@ add n n)))
JSON は、他のツールで処理するための中間表現です。
証明という一つの原本から、複数の言語の実装コードを取り出せる
── これも抽出という仕組みの持ち味です。
JSON への取り出しについて
JSON を指定した場合に出てくるのは、いわゆる key と value の JSON です。
実機の出力の冒頭は、次のようなキーと値の入れ子になっています。
{
"what": "decl:term", "name": "d",
"type": {
"what": "type:arrow",
"left": {
"what": "type:glob", "name": "nat", "args": [
ただし、これは実行できるプログラムではありません。
OCaml・Haskell・Scheme の３つは、そのままコンパイルして動かせるコードが出てきますが、JSON は違います。
記述されるのは、「double という項があり、その型は nat から nat への矢印で・・・」 という、プログラムの構造を機械可読な形で書き下したデータ です。
"what": "decl:term"（項の宣言）、"what": "type:arrow"（関数型）といったキーが、構文木のノードの種類を表しています。
用途は、他のツールへの受け渡しです。
Rocq から取り出した定義を、自前のコード生成器に読み込ませて別の言語へ変換したり、解析ツールで調べたりする場合の中間データとして使います。
人が読んで動かすためではなく、プログラムがプログラムを処理するための形式 です。
【発展篇】OCaml とはどんな言語か ── ML という家系の話
OCaml の出自は、定理証明の歴史と絡み合っています。
始まりは、1970年代のエディンバラ大学です。
計算機科学者ロビン・ミルナーが、LCFという証明支援システムを作るとき、証明の手順を書くための言語をあわせて設計しました。
その言語の名前が ML ── Meta Language（対象を操作するための言語）の略です。
つまり ML は、そもそも定理証明の道具を書くために生まれた言語 でした。
強い型検査で誤りを早く捕まえ、関数を自在に組み合わせ、場合分け（パターンマッチ）で構造を分解する
── この家風を受け継ぐ言語たちが、ML系と呼ばれます。
Caml は、この家系のフランス側の子孫です。
1980年代半ばに INRIA で設計されました。
場所は Rocquencourt。
本文で述べた、Rocq の新しい名前の由来になった、あの研究所の所在地です。
Rocq と OCaml は、生まれた場所まで同じ身内なのです。
OCaml は、Caml の現行の姿です。
1996年に、オブジェクト指向の機能を加えた Objective Caml として登場し、後に OCaml と改称されました。
型推論（型ヒントを書かなくても、処理系が型を割り出す仕組み）の強力さと、コンパイル後の実行速度で知られます。
Python との距離感でいえば、「型ヒントが最初から必須で、しかもほぼ自動で埋まり、実行前に検査され、速い Python」を想像すると、方向としては近い言語です。
第２部 ── コードで読む（最小の実例を全行解説）
ここからコードを読みます。必要な読み方は、次の表だけです。
| 書き方 | 役割 | Python での近い感覚 |
|---|---|---|
| Inductive 名前 : Type := | 新しい型を、作り方の一覧で定義する | Enum の定義に近い |
| Definition 名前 := 式 | 関数や値の定義 | def での関数定義 |
| Theorem 名前 : 主張 | これから証明する定理の宣言 | 近いものが無い（本記事の主役） |
| Proof. 〜 Qed. | タクティクによる証明の本体 | 近いものが無い |
| Extraction 名前 | 定義からコードを取り出す命令 | 近いものが無い |
コードの中の語は、
- 「予約語と記号」
- 「タクティクやライブラリの名前」
- 「プログラマが任意の名前を付けた箇所」
の３つに分けて、そのつど解説します。
実例１ ── まず、ふつうの Rocq を１つ
Inductive light : Type :=
| on
| off.
Definition flip (b : light) : light :=
match b with
| on => off
| off => on
end.
灯りの型を自作し、切り替えの関数を定義しています。
上から順に読んでいきます。
最初の３行が、型の定義です。
Inductive light : Type := は、「light という新しい型を、これから作り方の一覧つきで定義する」という宣言です。
Type は 「型の型」を指すライブラリの名前 です。
縦棒で並べた２行 が lightの値の作り方の一覧 で、「light の値は on と off の２つだけ」と読みます。
Python の Enum の定義に近い形です。
残りの５行が、関数の定義です。
Definition flip (b : light) : light := は、「flip は、light を受け取って light を返す関数」という宣言で、Python の型ヒント付きの def にあたります。
match から end までが場合分けで、on なら off を、off なら on を返します。
Python の match 文と、見た目までよく似ています。
このコードでプログラマが自分で名付けたのは、light、on、off、flip、b です。
Inductive、Definition、match、with、end、:=、=>、縦棒は予約語と記号で、
Type がライブラリの名前です。
ここまでのコードを見るかぎり、Rocq は、ごく普通の関数型言語です。
実例２ ── 定理を、タクティクで証明する
Theorem sample : 2 + 2 = 4.
Proof.
reflexivity.
Qed.
上から順に読んでいきます。
１行目が、定理の宣言です。
Theorem sample : 2 + 2 = 4. は、「sample という名前で、『2 + 2 = 4』という主張をこれから証明する」という宣言です。
型の欄に主張を書く、という定理証明の核心が、ここに現れています。
Proof. から Qed. までが、証明の本体です。
中身は reflexivity という１語だけです。
これが、タクティク ── Rocq の処理系への指示です。
reflexivity は、「左右を計算して、同じ形になることを確かめよ」という指示 で、処理系は 実際に $2 + 2$ を計算して $4$ に到達し、証明を完成させます。
Qed. は「証明終わり」の宣言 で、ここで処理系の検査が確定 します。
このコードでプログラマが自分で名付けたのは sample だけです。
Theorem、Proof、Qed は予約語、
reflexivity はタクティクの名前です。
Agda の記事をお読みの方は、違いに気づかれたはずです。
Agda では証明そのもの（refl という値）を中身の欄に手で書きました が、Rocq では 「確かめよ」という指示 を書きます。
指示の言葉を増やしていくと、処理系に任せられる範囲が広がっていく ── これが タクティク の流儀です。
Agda の記事をお読みの方も、細部は忘れておられるでしょうから、コードで比較します。
前回の記事で扱った Agda で、いま証明したのと同じ定理を書くと、次のようになります。
open import Data.Nat
open import Relation.Binary.PropositionalEquality
sample : 2 + 2 ≡ 4
sample = refl
最初の２行は、道具の読み込みです。
自然数と、等しさの記号（≡）、そして refl が手に入ります。
注目していただきたいのは、最後の２行です。
３行目は、Rocq の Theorem sample : 2 + 2 = 4. と同じ働きで、型の欄に主張を書いています。
そして４行目の refl が、証明そのもの です。
同じ定理の、Rocq のコードを並べます。
Theorem sample : 2 + 2 = 4.
Proof.
reflexivity.
Qed.
違いは、それぞれの語がコードの中で果たす役割です。
Agda の refl は、証明そのもの です。
sample = refl
この refl が、「 $2 + 2$ と $4$ は、計算すれば同じ形になる」という事実の 証明の中身 です。
定理証明エンジニアは、sample = の右側に完成した証明を置いています。
Agda の処理系は、置かれたものが本当に証明になっているかを検査するだけです。
一方、Rocq の reflexivity は、証明ではありません。
Proof.
reflexivity.
Qed.
Proof. と Qed. に挟まれたこの reflexivity は、「両辺を計算して、同じ形になることを確かめよ」という 作業の指示 です。
定理証明エンジニアが書いたのは指示だけで、証明の中身は、この指示を受けた Rocq の処理系が組み立てます。
つまり、Agda では人が証明を作って処理系が検査し、Rocq では人が指示を出して処理系が証明を作ります。
指示の言葉を増やしていくと、処理系に任せられる範囲が広がっていく ── これが タクティク の流儀です。
３つで一揃い ── 実演を、読み直す
ここまでの２つの実例で、道具が揃いました。
型の定義（実例１）と、タクティクによる証明（実例２）です。
全体像の節でお見せした実演は、この２つに「取り出し」を加えたものでした。
いま読み返せば、全行の意味が分かるはずです 。
- Definition の行は、実例１と同じ関数の定義、
- Theorem から Qed. まで は、実例２と同じ定理の証明、
- 最後の Extraction の３行 が、Rocq ならではの取り出しの命令です。
小さな例なので、取り出したコードもささやかでした。
しかし、この同じ仕組みを何万行の規模で回すと何が建つのでしょうか？
それが次の第３部です。
第３部 ── 実務の成果（出典つき）
ここに挙げるのは、論文または公開情報で確認できた成果です。
CompCert ── 検証済みの Cコンパイラ
コンパイラは、プログラムをコンピュータが直接実行できる機械語へ翻訳する道具です。
翻訳が間違っていたら、どれだけ丁寧に書いたプログラムも、書いたとおりには動きません。
CompCert は、この翻訳の正しさを Rocq（当時 Coq）で証明したうえで、コンパイラ本体を抽出で取り出した、検証済みの Cコンパイラです。
フランスの計算機科学者グザヴィエ・ルロワらが開発し、2009年に代表的な論文が発表されました。
説得力のある傍証があります。
2011年、自動生成のテストでコンパイラのバグを探す研究（Csmith）が発表され、広く使われる主要なコンパイラから多数のバグが報告されました。
CompCert からもバグは見つかりましたが、そのすべては、当時まだ検証が及んでいなかった周辺部分のものでした。検証済みの部分からは、誤ったコードを生ませる誤りが１件も見つからなかったのです。
研究チームは、約６年分のCPU時間を注いでも検証済み部分を破れなかったと記し、証明の枠組みの中でコンパイラを開発することの利益を裏づける結果だと結論しています。
これは、テストが正しさを証明したという話ではありません。
独立して実施したテストが、証明という手段の強さを外から照らした、という関係です。
CompCert は現在、商用ライセンスでも提供されており、航空分野をはじめとする組み込みシステムでの利用が報告されています。
2022年には、開発チームが計算機科学の主要な賞のひとつ、ACM ソフトウェアシステム賞を受賞しました。
Fiat-Crypto ── 検証済みの暗号コード
暗号 のプログラムは、誤りが許されない世界の代表 です。
しかも、速度のために手作業で最適化された難解なコードになりがちで、検査が困難でした。
Fiat-Crypto は、楕円曲線暗号の中核の計算 を Rocq の上で証明 し、そこから各環境向けの高速なコードを生成 する研究です。
そして、生成された検証済みの実装（Curve25519 と P-256 という、広く使われる楕円曲線の計算）は、Google の暗号ライブラリ BoringSSL に採用されました。
BoringSSL は Chrome や Android を支えるライブラリ です。
つまり、Rocq の証明から生み出されたコードが、日常のブラウザ通信の中で動いています。
数学の金字塔 ── 四色定理と奇数位数定理
抽出とは別の軸でも、この言語には実績があります。
数学の形式化 です。
「どんな地図も４色で塗り分けられる」という四色定理は、人間の手に負えない場合分けの多さで知られた難物でした。
2005年、ジョルジュ・ゴンティエらが Coqの処理系の上で、全証明を検査し切りました。
続いて2012年には、四色定理と同じくジョルジュ・ゴンティエが率いるチーム（Microsoft Research–INRIA 共同研究センター）が、群論の大定理である奇数位数定理 （証明が数百ページに及ぶ、20世紀数学の金字塔のひとつ）の形式化を、Coqの上で完了 させました。
用いられたのは、SSReflect という拡張 と、Mathematical Componentsライブラリ です。
四色定理の形式化のために開発された道具立てが、そのまま奇数位数定理へ発展した流れ です。
この記事で、このあと、「学び方」の節で挙げる日本語書籍『Coq/SSReflect/MathComp による定理証明』は、まさにこの系譜の道具を扱った本です。
ところで数学の形式化では、現在 Lean 4 の Mathlib が大きな存在感を持っています。
しかし、「巨大な数学の証明をコンピュータで検査し切れる」ことを世界に強く印象づけた代表例は、Rocq（当時の Coq）の仕事でした。
【歴史の補足説明】巨大な証明の機械検査 ── この系譜の外の仕事たち
「代表例」と書いたのには、理由があります。
巨大な証明の機械検査は、この言語の系譜だけの仕事ではないからです。
-
Mizar ── 1970年代に始まった最古参級のプロジェクトで、数学の定理を数十年にわたり単一のライブラリに蓄積してきました
-
Isabelle ── 素数定理の形式化（2004年）をはじめ、大型の数学の機械検査で長い実績を持つ定理証明系です。後年には、検証済み OS カーネル seL4（2009年）という、ソフトウェア検証の金字塔もこの言語の上で建ちました
- HOL Light ── ケプラー予想の形式化プロジェクト Flyspeck（2014年完了）の主力でした。球を最も密に積む方法についての、場合分けの巨大な証明です
つまり四色定理（2005年）は、単独の「世界初」ではなく、複数の系譜が並走してきた歴史の中の、特に広く知られた一峰 です。
なお、この３つはいずれも過去の遺物ではなく、現在も開発と利用が続く現役の処理系です。
Mizar は2025年５月にライブラリの新版が公開され、蓄積された論文は1,500本を超えました。
Isabelle も2025年３月に最新版（Isabelle2025）がリリースされています。
巨大な証明の機械検査は、特定の言語が独占してきた分野ではなく、複数の系譜が並走しながら現在も続いている営みです。
初学者が今から学ぶ価値はあるか
３つのうち、Isabelle には明確にあります。 残る２つは、目的が限定されます。
-
Isabelle ── 学ぶ価値が高い言語です。使われている領域は２つあります。１つは ソフトウェアとハードウェアの形式検証の実務 で、seL4 を核とする OS・組込み・航空宇宙・セキュリティの分野において、産業利用の実績が最も厚い定理証明系のひとつです。もう１つは 数学の形式化 で、Archive of Formal Proofs という査読つきの巨大な証明アーカイブが、Mathlib と並ぶ規模で運用されています。加えて、sledgehammer という自動証明の道具が強力で、タクティクを覚える負担が比較的軽い という学習上の利点もあります。就職・研究の両面で、Lean 4 と Rocq に次ぐ第３の選択肢として実質的な意味があります。
-
HOL Light ── 学ぶ価値は限定的です。使われている領域は、ケプラー予想のような 大規模な数学の形式化 の一部プロジェクトと、Intel の浮動小数点演算の検証 です（開発者ジョン・ハリソンが Intel に在籍していた経緯で、CPU の算術回路の正しさの検証に使われた実績があります）。ただしコミュニティが小さく、教材も少ないため、初学者の入口としては勧めにくい言語です。「カーネルが極小で、信頼できる基盤とは何かを学ぶ教材」としての価値が主になります。
- Mizar ── 学ぶ価値は最も限定的です。使われている領域は 純粋数学の形式化 のみで、ソフトウェア検証には使われません。特徴は「人間が読める数学の文章に極めて近い記法」で、その設計思想は Isabelle の Isar 記法などに影響を与えました。ただし処理系が単一で、抽出のような応用機能もなく、実務との接点がありません。数学の形式化そのものを研究対象にする方以外には、勧めにくいというのが実情です。
要約すると、今から学ぶなら Isabelle です。
他の２つは、Intel 系の検証研究や、数学の形式化の歴史と記法の研究といった、特定の目的がある場合に限られます。
Isabelle については、追って独立した言語紹介の記事を公開予定です。
第４部 ── Lean 4・λProlog との関係
連載で紹介してきた言語たちと、Rocq の関係を整理します。
Lean 4 と ── 同族言語同士の間の役割の分業
Lean 4 と Rocq は、理論の土台もタクティクの流儀も近い、いわば同族です。
利用者数の統計は無く、どちらが上という話はできません。言えるのは、役割の違いです。
数学の定理を書き溜めるライブラリの規模と、AIとの接続では、Lean 4 が現在の中心的存在です。
その一方で、証明からプログラムを取り出す道具立てと、その上に建った実務の成果（CompCert、Fiat-Crypto）では、Rocq に厚い蓄積があります。
なお、Lean 4 にも、自分のコードを高速に実行する仕組みはあります。
違いは方向性です。
- Lean 4 ： 「証明のための言語で、そのまま汎用プログラムも記述できる」方向
- Rocq ： 「証明から、別の言語のプログラムを取り出す」方向
λProlog と ── 内側で働く言語
本連載の λProlog の記事で紹介したとおり、Rocq にはタクティクなどの拡張を書くための仕組みとして、λProlog 系の言語（Elpi）を使う道があります。
証明を検査する言語の内側で、別の論理プログラミング言語が道具作りを担う 関係です。
Elpi は、処理系と主要な道具を一括で導入できる公式パッケージ（Rocq Platform）に同梱されており、パッケージの名称も、Coq から Rocq に言語名が変更されたのと歩調を合わせて、Coq-Elpi から Rocq-Elpi へと、名称が改められています。
学び方のロードマップ ── 知識ゼロから、どう学ぶか
『Coq/SSReflect/MathComp による定理証明』（森北出版、2018年）という日本語の書籍 があります。
また、世界標準の教科書 Software Foundations（ソフトウェアの基礎）には、有志による日本語訳が公開されています。
日本語で学び始められることは、この言語の強みです。
定番の順路
-
Software Foundations を頭から進める。無料公開の定番教科書で、演習を解きながらタクティクの語彙が増えていく作りです
- 手元の環境か、ブラウザで動く処理系（jsCoq）で、本記事の実例を再現する。書いて動かした行だけが、身につきます
- 抽出に興味が向いたら、公式ドキュメントの Extraction の章と、CompCert の論文へ進む
- 壁に直面したら、公式のコミュニティ（Zulip や Discourse）で質問する
まとめ
- Rocq は、1980年代に INRIA で生まれた定理証明の老舗である。長年 Coq の名で知られ、2025年に Rocq へ改名された
- 最大の個性は抽出 ── 条件を満たす値を組み立てて見せる流儀の証明から、正しさの議論を消し、計算の手順だけを OCaml などの動くコードとして取り出せる
- この仕組みの上に、検証済み C コンパイラ CompCert と、Google の暗号ライブラリに採用された Fiat-Crypto という実務の成果が実在する
- 証明はタクティクで書く。証明を関数として手で書く Agda とは対照的で、Lean 4 とは同族の分業関係にある
- 日本語の書籍を含む学習資産が厚く、知識ゼロからの入口が整っている
関連記事
出典
- The Rocq Prover（公式サイト） ── 言語の公式情報と、Coq からの改名の経緯
- "Formal verification of a realistic compiler"（Leroy、Communications of the ACM、2009年） ── CompCert の代表論文
- "Finding and Understanding Bugs in C Compilers"（Yang、Chen、Eide、Regehr、PLDI 2011） ── Csmith によるコンパイラのバグ探索の研究
- CompCert（AbsInt 社の製品ページ） ── 商用提供の現況と、ACM ソフトウェアシステム賞、Csmith 論文からの引用
- "Simple High-Level Code for Cryptographic Arithmetic"（Erbsen ほか、IEEE S&P 2019） ── Fiat-Crypto の論文
- "Formal Proof ── The Four-Color Theorem"（Gonthier、Notices of the AMS、2008年） ── 四色定理の形式化の解説
- Software Foundations（Pierce ほか） ── 定番教科書
- ソフトウェアの基礎（Software Foundations 日本語訳） ── 有志による日本語訳の公開ページ
検証環境:本記事の Rocq のコードは、Coq 8.18.0（Ubuntu 24.04、OCaml 4.14.1）で、2026年8月7日に検査の通過を確認しました。実演の Extraction の出力は、この環境の実機の出力をそのまま掲載しています。第２部の Agda のコードは、Agda 2.6.3+agda-stdlib 1.7.3 で、同日に検査の通過を確認しました。
さらに、改名後の Rocq 9.0.1（ソースからビルドした、The Rocq Prover と名乗る実機）でも、本記事のコードが無修正のまま検査を通過し、Extraction の出力も一字一句同一である ことを、2026年8月8日に確認しました。旧来のコマンド（coqc）と、統合された新コマンド（rocq compile）の両方で確認しています。