Jane Streetによる形式手法とプログラミングの未来について

Jane Streetは、形式手法（formal methods）に対する組織的な姿勢を、懐疑的な立場から、ソフトウェア開発ライフサイクルにこれらの技術を統合するための専用チームを構築するという積極的な投資へと転換させています。この変化は、エージェンティック・コーディング（agentic coding）の出現によって推進されており、これは形式証明の作成コストを下げると同時に、AIが生成したコードに対する厳格な検証の必要性を高めています。

Agentic Coding as a Catalyst for Formal Methods

Agentic codingは、実装のコストと信頼性へのニーズの高まりの両方に対処することで、形式手法の費用対効果の分析を根本的に変えました。

Reducing the Cost of Proofs

歴史的に、形式手法は非常に高価でした。例えば、seL4マイクロカーネルは、8,700行のC言語のコードを検証するために25人年の労力を必要とし、コードの1行につき約23行の証明が必要でした。AIエージェントは現在、証明のアイデアを証明システムが満たす形式にエンコードするという退屈な作業を自動化することで、この障壁を低くし、これらのツールを生産的に使用できる開発者の層を広げています。

Solving the AI Verification Bottleneck

AIモデルは機能的なコードを書く能力がincreasingly capable（ますます向上）していますが、しばしば「slop（スロップ）」、つまり、過度に複雑であったり、微妙なバグを含んでいたり、コードベースの不可欠な不変条件（invariants）に違反したりするコードを生成します。これは、AIが生成したコードが本番環境で使用可能であることを確認するために人間が多大な時間を費やさなければならないという、検証のボトルネックを生み出します。形式手法は、テストだけでは提供できない数学的な保証を提供することで、この負担を軽減するためのスケーラブルな方法を提供します。

Enhancing Agent Feedback Loops

AIエージェントは正確なフィードバックに依存しています。プロパティベーステストやファジングは価値がありますが、プログラムの全状態空間をカバーすることはできません。形式手法は普遍的な保証（$orall$ 量化子）を提供し、開発者がデータレースやクロスサイトスクリプティングの脆弱性といった、クラス全体としてのバグを完全に排除することを可能にします。この厳格なフィードバックループは、エージェントの複雑な問題を解決する能力を向上させます。

Strategic Implementation at Jane Street

Jane Streetは、自社のツールへの制御権と内部文化により、形式手法を進展させる独自のポジションにいると考えています。

Language Control and OxCaml

使用する言語（具体的にはOxCaml）に対して深い制御権を維持することで、Jane Streetは、証明指向の技術をより良くサポートするために言語を修正することができます。潜在的な方向性は以下の通りです：

プロパティのモジュール式仕様を型システムに直接統合すること。
所有権（ownership）と可変性（mutability）のための型レベルの制約を追加すること。
証明技術を言語の構文に直接組み込むこと。

A Culture of Type-System Adoption

新しいツールを採用するよう開発者に説得することが課題となる多くの組織とは異なり、Jane Streetには、より洗練された型システム機能への要求が活発なプログラマーのコミュニティがあります。この内部的な意欲は、、 firm が、即時的な短期的な改善と、野心的な長期的なビジョンを実験的に試すことを可能にします。

Industry Perspectives and Counterpoints

Jane Streetの動きに関するコミュニティの議論は、形式手法の適用におけるいくつかの重要な緊張関係を浮き彫りにしています。

The Mapping Problem and Domain Limits

一部の批評家は、形式手法が最も効果的なのは、仕様とドメインの対応が1:1である決定論的なアルゴリズムを実装する場合であると主張しています。探索的な作業やUI開発においては、「地図は領土ではない（the map is not the territory）」、つまり形式的な仕様が実用的でない場合があります。あるコメント主が指摘したように：

"In theory, there is no difference between theory and practice. In practice..."