Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

数学の世界を、巨大で古めかしい都市だと想像してみてください。何世紀もの間、人々は自分たちで論理の家を建ててきましたが、しばしば異なる設計図を使用していたため、道具を共有したり、新しい街区を共に建設したりすることが困難でした。そこに「Mathlib」が現れました。これは、世界中の数学者たちが、同じ言語と規則を用いて証明を構築することに同意した、壮大で中央集権的な図書館です。それは、複雑で孤立したアイデアを、共有され、検証された都市景観へと変えるユニバーサルな翻訳機のようです。そこでは、どのように橋が架けられたのかを誰もが正確に確認でき、その橋が崩落しないという信頼を得ることができます。

次に、コンピュータサイエンスが、建設を待っている次の偉大な都市であると想像してください。それは、私たちが機械にどのように考えさせ、動かし、問題を解決させるかを研究する学問です。しかし、かつての数学の都市と同様に、コンピュータサイエンスもまた、しばしば孤立したワークショップの集合体となってきました。この論文は、Mathlibが数学に対して行ったことを、コンピュータサイエンスに対しても実現しようとする新しいプロジェクト、「CSLib」を紹介しています。ここでの大きな問いは、シンプルでありながら極めて重大です。コンピュータサイエンスの「背骨」となるものが、ソフトウェアやモデルを形式的に検証できるほど、強固で標準化されたものになり得るでしょうか？ もしそれが実現すれば、私たちは単にエラーを見つけるためにテストだけに頼るのではなく、数学的に検証された特性を持つデジタルシステムを構築できるようになるのです。

デジタル都市の新しい背骨

CSLibを、成長するデジタル都市の「中枢神経系」と考えてください。都市がスカイスクレイパーや橋を支えるために頑丈な背骨を必要とするように、コンピュータサイエンスも、私たちが日々使用する複雑なソフトウェアを支えるための、検証された規則の強固な基礎を必要としています。この論文は、その背骨の設計図を提示するものです。これは単にランダムな部屋をいくつか建てるのではなく、基礎となる原理、動作規則、そしてセマンティック・フレームワーク（これは、プログラムについて語るための「辞書と文法」を意味する、少し専門的な言い方です）を敷設し、この新しいライブラリに参加する全員が同意して使用するものを提供します。

著者たちは、巨人の肩の上に立ち、具体的にはMathlibの足跡を辿っています。彼らは、純粋数学において成功したのと同じレシピを、複雑で実用的なコンピュータサイエンスの世界に適用しようとしています。目標は、プログラミング言語やソフトウェアモデルに関するアイデアを、どこでも、誰でも保存、チェック、再利用できる場所を作ることです。

道具立て

このライブラリを機能させるために、論文ではデジタル都市の建設機材のような役割を果たす、巧妙なツールを紹介しています。

第一に、彼らは再利用可能なセマンティック・インターフェースを構築しました。例えば、ビデオゲームのキャラクターがどのように動くかを説明しようとしているとします。アニメーションの全フレームを一つずつ記述することもできますが、「プレイヤーが『A』を押せば、キャラクターはジャンプする」といった標準的な一連のルールを使うこともできます。CSLibにおいて、著者たちは2つの特定の動きに対して標準的な「ルールブック」を作成しました。一つは簡約（reduction）（プログラムがどのようにステップごとに自身を単純化するか）、もう一つはラベル付き遷移システム（labelled transition systems）（プログラムがどのようにある状態から別の状態へ移動するか、例えば信号機が赤から緑に変わるような動き）です。これらは単発の記述ではありません。これらは再利用可能なインターフェースです。つまり、新しいプログラミング言語について何かを証明したい場合、車輪の再発明をする必要はありません。既存の信頼できるルールブックに、新しい言語をプラグインするだけでよいのです。

第二に、論文は**証明の自動化（proof automation）**を強調しています。かつて、ソフトウェアが正しいことを証明することは、壁の一枚一枚のレンガを手作業でチェックするようなものでした。それは時間がかかり、ヒューマンエラーが発生しやすいものでした。著者たちは、スーパーファストなロボット助手のように機能するツールを提供しました。この自動化は証明のチェックを支援し、人間がコードの一行一行を凝視し続けなくても、論理が成立していることを保証します。それは、決して疲れることのない、論理のためのスペルチェッカーを持っているようなものです。

第三に、彼らはCI/テスト・サポートを確立しました。ソフトウェアの世界において「CI」とは「継続的インテグレーション（Continuous Integration）」を指し、これは基本的にはセーフティネットです。誰かがライブラリに新しい要素を追加するたびに、自動化されたシステムが、それが他の部分を壊していないかをチェックします。論文では、このシステムが新しいコンピュータサイエンスのライブラリを、古い数学のライブラリ（Mathlib）と互換性を保つように設計されていることが述べられています。これは、新しいデジタルハイウェイが既存の数学の橋と完璧に接続されるようにし、二つの世界の間で交通がスムーズに流れるようにすることに似ています。

実際に何が存在するのか？

この論文は単にツールについて語るだけでなく、それらがすでにどのように使われているかを示しています。著者たちは、この新しいフレームワーク内における言語とモデルの**最初の実質的な発展（first substantial developments）**を寄稿しました。これは、彼らが単に足場を組んだだけでなく、実際に最初のいくつかの建物を建設し始めたことを意味します。彼らはプログラミング言語やモデルの現実世界の概念を取り上げ、それらを新しいシステムを用いて見事に形式化しました。

しかし、達成された範囲を理解しておくことが重要です。論文では、これらを「基礎となる原理」および「初期の開発」として提示しています。これは、このアプローチが有効であり、将来に向けた強固なフレームワークを提供していることを示唆していますが、コンピュータサイエンスのあらゆる問題を解決したと主張しているわけではありません。この作業は「急速に成長している」ライブラリとして記述されており、これは、まだ建設中である、生きているプロジェクトであることを意味しています。著者たちは、基礎が強固であり、最初の部屋には家具が備えられていることを示していますが、都市の完成はまだ先なのです。

なぜそれが重要なのか

では、なぜ好奇心旺盛なティーンエイジャーが、形式化されたコンピュータサイエンスのライブラリに関心を持つ必要があるのでしょうか？ それは、段ボールで作られた家と、鋼鉄で作られた家の違いだからです。今日のソフトウェア作成において、私たちはしばしば、それが壊れるかどうかを見るためにテストを行います。もし壊れなければ、安全であると仮定します。しかし、CSLibがあれば、ソフトウェアのルールとモデルを厳密にチェックできる、共有された検証済みのライブラリを作ることが目標となります。これらのアイデアを集約し、チェックプロセスを自動化するツールを提供することで、著者たちは、重要な特性を数学的に検証できるソフトウェア開発への道を切り拓いています。

論文は、これらのアイデアを集約し、チェックプロセスを自動化するツールを提供することで、私たちのデジタル世界の「背骨」が壊れることのないものにできると主張しています。それは、コーディングの混沌が数学の秩序によって制御され、単に機能的なだけでなく、根本的に信頼できるデジタル風景を生み出すという、遊び心にあふれた野心的なビジョンなのです。