あなたは、デジタルな城を守るための超強力な要塞を築こうとしていると想像してください。コンピュータサイエンスの世界では、これらの要塞は**プログラム論理（program logics）**と呼ばれます。これらは、ソフトウェアがクラッシュしたり、秘密を漏洩したり、あるいは奇妙な挙動をしたりすることが決してないことを証明するために、数学者やプログラマーが使用する厳格なルールの集合です。

長い間、これらの要塞を築くことは、一つひとつのレンガを手作業で彫り出すようなものでした。例えば、新しい機能（例えば、停電への対処（クラッシュリカバリ）や、海を越えて他のコンピュータと通信する方法（分散システム））を追加したい場合、ゼロからやり直さなければなりませんでした。それは、要塞を単に「使う」ために必要なスキルとは全く異なる、特別な種類の「レンガ積み」のスキルを必要としました。それは困難で、時間がかかり、古い要塞のレンガを新しい要塞を作るために再利用することも容易ではありませんでした。

大きなアイデア：「エフェクトハンドラ」ツールキット

Zichen Zhang、Simon Oddershede Gregsen、Joseph Tassarottiによるこの論文は、これらの要塞を築くための新しい方法を提案しています。レンガを手作業で彫る代わりに、彼らは**エフェクトハンドラ（effect handlers）**と呼ばれる魔法の道具を使用します。

エフェクトハンドラを、ゲームのカスタマイズ可能なルールブックだと考えてみてください。標準的なビデオゲームでは、ジャンプや射撃のルールはゲームエンジンにハードコードされています。しかし、エフェクトハンドラを使うと、ゲームエンジンは「『ジャンプ』が何を意味するかはまだ分かりません。誰かが教えてくれるのを待っています」と言います。すると、プログラマーは小さなスクリプト（ハンドラ）を書いて、「よし、プレイヤーがジャンプしようとしたら、一瞬浮かせよう」と指示を出すことができます。

著者たちは、ルールが一切ない、この「指示待ち」機能だけを持つFicusLangという極めて小さな空の言語を構築しました。そして、以下のような事柄のためのルールを「作成」するためのハンドラを書き上げました。

• メモリ: プログラムがどのように物事を記憶するか（例：付箋）。
• 並行スレッド: プログラムがどのように多くのことを同時に行うか（例：複数の鍋を操るシェフ）。
• クラッシュ: 電源が切れて戻ってきたときに何が起こるか。
• 分散システム: コンピュータが不安定なネットワーク越しにどのように通信するか。

魔法のトリック：積み上げること

最も素晴らしい部分は、彼らが単にこれらのルールを作っただけでなく、それらを「証明」したことです。彼らは空の言語からスタートし、「メモリ」のためのハンドラを書き、Ficusという論理システムを使用して、そのメモリハンドラが正しく動作することを証明しました。一度このメモリハンドラが証明されると、それを使って「並行性」のハンドラを構築することができました。

これは家を建てるようなものです。まず、基礎がしっかりしていることを証明します。次に、そのしっかりした基礎を使って、1階部分を築きます。一度その1階が安全であると証明されたら、その1階を使って2階部分を築きます。このように構築されたため、機能を簡単に組み合わせることができました。もしプールとガレージの両方がある家が欲しければ、基礎全体を再構築することなく、「プールハンドラ」と「ガレージハンドラ」を組み合わせるだけでよかったのです。

より強力なルールと新しい仕掛け

これらのルールをハンドラを使って基礎から構築したことで、彼らは従来の方法よりも強力なルールを作れることが分かりました。

• 「一時停止」のトリック: 標準的な並行プログラミングでは、コンピュータは他のタスクに切り替えるために、あらゆる微細な瞬間にタスクを停止させることができます。これは、追跡が非常に困難な混乱を生み出します。著者たちのハンドラは、特定の「エフェクト」（例えば、ファイル読み込みのリクエストなど）が発生したときにのみタスクを切り替えます。彼らは、この「求められたときだけ一時停止する」方法が、「いつでも一時停止できる」方法と同等の安全性を持つことを証明しましたが、後者よりも推論がはるかに容易であることを示しました。
• 「水晶玉」（予言変数）: プログラムが安全であることを証明するために、ランダムなイベントが何をするかを、それが起こる前に知っておく必要がある場合があります。著者たちは「水晶玉」エフェクトハンドラを作成しました。これにより、証明において「この乱数は5になると予測する」と言い、後でそれが正しかったかどうかをチェックすることができます。彼らは、巨大なグローバルな水晶玉から、特定の変数に対するローカルな水晶玉を作れること、さらにはプログラマが追加のコードを書かなくても、メモリ操作に対して自動的に水晶玉が現れるようにできることを示しました。

「関係的」論理：双子のテスト

この論文は、RelFicusという新しいツールも導入しています。想像してみてください、あなたにはプログラムAとプログラムBという、全く同じ双子がいます。両方に同じ入力を与えたとき、たとえ一方がもう一方の少し異なるバージョンであったとしても、常に同じように振る舞うことを証明したいとします。

RelFicusは、これら2つのプログラムを頭の中で並行して実行（「ゴースト状態」や想像上のリソースを使用）することで、それらが双子であることを証明できる論理です。これは、彼らの新しい「求められたときだけ一時停止する」並行ハンドラが実際に安全であることを証明するために不可欠でした。彼らはこの双子のテストを用いて、余分な「一時停止ポイント（プリエンプション）」を追加してもプログラムの結果が変わらないことを証明し、これにより、よりシンプルで使いやすいモデルの正当性を裏付けました。

彼らがやらなかったこと（および拒絶したもの）

この論文が何ではないかを知っておくことは重要です。

• 彼らは、従来の論理の構築方法（「手作業によるレンガ彫り」法）が役に立たないと言っているわけではありません。単に、それが再利用しにくく、拡張しにくいと言っているのです。
• 彼らは、これらの論理を構築するために、複雑で抽象的な数学構造（以前の研究で言及された「ITrees」など）を理解する必要があるという考えを拒絶しています。彼らのアプローチは、開発者にとってすでに馴染みのある標準的なプログラミング概念（ハンドラ）を使用しているため、よりアクセスしやすいと主張しています。
• 彼らは、コンピュータセキュリティのあらゆる問題を解決したと主張しているわけではありません。彼らはメモリ、並行性、クラッシュ、分散システムのためのハンドラを具体的に構築しましたが、他の機能には新しいハンドラが必要になる可能性があることも認めています。

どの程度確実なのか？

著者たちは非常に自信を持っていますが、同時に精密でもあります。彼らは単にこれが機能する可能性を「示唆」したのではなく、証明しました。

• 彼らは論理システム全体をRocq Prover（数学的証明をチェックするコンピュータプログラム）というツールで記述しました。
• 彼らは**Adequacy（妥当性）**という定理を証明しました。これは、論理がプログラムは安全であると言えば、そのプログラムは実際に停止（スタック）せずに動作することを保証するものです。
• 彼らは、新しい並行モデルが標準的でより複雑なモデルと等価であることを証明しました。
• 彼らは、グローバルなバージョンから派生させることで「水晶玉（予言）」機能が機能することを示し、数学的な整合性が保たれていることを証明しました。

まとめ

この論文は、コンピュータサイエンティストに、濡れた粘土の山ではなく、レゴブロックを与えているようなものです。以前は、新しいタイプの城を作りたい場合、自分で粘土を混ぜ合わせなければなりませんでした。今では、「メモリ」、「クラッシュ」、「ネットワーク」のための、あらかじめ作られ、テスト済みのレンガがあります。それらをカチッとはめ込むことができ、その数学的根拠によって、城が崩れないことが保証されます。これにより、複雑で安全なソフトウェアを構築することは、孤独な芸術プロジェクトではなく、誰もが最高のパーツを再利用できる、共同建設現場のようになります。