1959年モスクワのソート問題から2026年Amazon障害まで — Tony Hoareが遺したもの
1959年モスクワのソート問題から2026年Amazon障害まで — Tony Hoareが遺したもの
1959年モスクワ、26歳の青年が直面した問題
1959年、26歳の英国青年トニー・ホーア(Tony Hoare)はモスクワ国立大学にいた。コルモゴロフ研究室でロシア語-英語の機械翻訳を研究していた彼に、一つの実務的問題が与えられた。ロシア語の単語を辞書順に並べ替えなければならなかった。
当時知られていた方法はバブルソート(bubble sort)だった。ホーアはこれが”obviously rather slow”だと感じた。そこで別の方法を考え始めた。アイデアは単純だった。基準要素(pivot)を一つ取り、それより小さいものは左へ、大きいものは右へ置き、両側を同じ方法で再び並べ替える。再帰的に。
これがクイックソート(Quicksort)の誕生だった。
問題は、当時のプログラミング言語が再帰をサポートしていなかったことだ。ホーアが使っていたElliott BrothersのMercury Autocodeには、再帰呼び出しという概念自体がなかった。クイックソートは頭の中だけに存在するアルゴリズムだった。1961年、ALGOL 60が再帰をサポートして初めて、コードとして実装できた。アイデアが2年間待った形である。
6ペンスの賭けとアルゴリズムの経済学
ホーアがElliott Brothersに入社したあとのエピソードが伝えられている。彼は上司に「既存より速いソートアルゴリズムがある」と主張した。上司の反応は簡潔だった。
“I bet you sixpence you don’t!”
ホーアは証明し、6ペンスを受け取った。
6ペンスは当時の基準でも少額だった。しかしクイックソートが世界にもたらした経済的価値は計測不能なほど大きい。数字で見るとこうだ。
100万件のデータを並べ替える際、バブルソートのO(n²)は約1兆回の演算を要する。クイックソートのO(n log n)は約2千万回で済む。5万倍の差だ。10億件に上がれば差は3,300万倍になる。
Unixのqsort()、C++のstd::sort、JavaのArrays.sort — これらすべての基礎がクイックソートである。67年間、世界中の数百万台のサーバーで毎日数兆回実行され続けてきた。比喩するなら、ソウルから釜山まで毎回歩いていた世界にKTXを敷いたようなものだ。しかも全てのコンピュータに同時に。
その対価は6ペンスだった。
「単純さこそが信頼性である」
1980年、ホーアはチューリング賞を受賞した。彼の受賞講演から生まれた格言は、ソフトウェアエンジニアリングの古典となった。
「ソフトウェア設計には二つの方法がある。一つは欠陥が明白に存在しないほど単純に作ることであり、もう一つは明白な欠陥がないほど複雑に作ることである。」
この一文の核心は「明白に」と「明白な」の位置の差にある。前者は構造そのものが単純なので欠陥が存在し得ないことが自明な状態だ。後者は複雑ではあるがまだ欠陥が見つかっていない状態だ。両者の差は根本的だ。一つは証明であり、もう一つは希望である。
ホーアはここで止まらなかった。
「信頼性の代価は、極度の単純さを追求することである。これは非常に裕福な人々が最も支払いを嫌がる代価だ。」
大規模システムを運用する組織ほど単純さを選択しがたいという逆説。予算が十分だから複雑な解決策を選び、複雑さが積み重なるとさらに多くの予算を投入する悪循環。ホーアはすでに40年前にこのパターンを正確に指摘した。
そしてもう一つの観察:
“Inside every large program is a small program struggling to get out.”
あらゆる巨大なプログラムの中には、抜け出そうともがく小さなプログラムがある。複雑さは本質ではなく蓄積物だという意味である。
CSPとHoare Logic — 現代プログラミング言語に遺した遺産
ホーアの貢献はクイックソートにとどまらない。
**CSP(Communicating Sequential Processes)**は1978年に発表された並行プログラミングモデルだ。核心アイデアは単純だ。プロセスが共有メモリの代わりにメッセージをやり取りして通信する。この概念は数十年後のプログラミング言語の基盤となった。
Go言語のgoroutineとchannelはCSPを直接継承したものだ。Goコミュニティの格言”Don’t communicate by sharing memory; share memory by communicating”は、ホーアのCSP哲学を一文に圧縮したものに他ならない。Erlangのactor model、Rustのfutures、Clojureのcore.async — すべてホーアが蒔いた種から育った木々である。
Hoare Logic(ホーア論理)はプログラムの正しさを数学的に証明する体系だ。事前条件(precondition)、プログラム、事後条件(postcondition)から構成される、いわゆる「ホーア三つ組(Hoare triple)」は形式検証(formal verification)の基礎となった。
{P} C {Q}「条件Pが真である状態でプログラムCを実行すると、条件Qが真になる。」
この単純な形式がDafny、Lean、F*、Frama-Cのような現代の検証ツールの理論的土台だ。ホーアが1969年に提案したこの体系が、57年経った2026年に最も切実に必要とされているという事実については、後半で改めて述べる。
「実装があまりに簡単だったので、誘惑を断りきれませんでした」
ホーアの偉大さの一つは、自身の過ちを認める勇気だった。
2009年、QCon Londonでホーアはこう告白した。
「私はこれを自分の10億ドルの過ちと呼びます。1965年にnull参照を発明したことです。当時私はオブジェクト指向言語(ALGOL W)の参照のための型システムを設計していました。目標は、コンパイラが自動的に確認し、すべての参照の使用が絶対的に安全であることを保証することでした。しかし、null参照を入れる誘惑を断りきれませんでした。実装があまりに簡単だったからです。」
「実装があまりに簡単だったから」。この一文にソフトウェア史の核心的教訓が込められている。
null参照はその後60年間、数え切れないNullPointerException、segfault、システム障害の原因となった。ホーア自身の推算で「10億ドル」だが、実際の被害額はそれをはるかに超えるだろう。
しかし彼の告白は変化を生んだ。現代のプログラミング言語はホーアの過ちから学んだ。
- Rust:
Option<T>でnullを完全に排除した。値が存在しない可能性のあるケースを型システムが強制的に処理させる。 - Kotlin: 変数は基本的にnon-nullable。nullを許容する型は
String?のように明示的にopt-inしなければならない。 - Swift: Optional、
guard let、if letパターンでnull安全性を保証する。 - TypeScript:
strictNullChecksオプションでnull/undefinedを型レベルで管理する。
ホーアが1965年に犯した過ちを2009年に公に認め、その告白がプログラミング言語設計の方向を変えた。過ちを隠すのではなく直視することが真の前進を生むという証である。
2026年3月、Amazon — 同じ誘惑の反復
2026年3月、Amazonで連鎖的な障害が発生した。
3月2日、AIが寄与したコードによる障害が発生した。結果は12万件の注文損失と160万件のエラー。3月5日には6時間の大規模障害が続いた。チェックアウト、ログイン、価格表示までが麻痺した。さらにすでに2025年12月には、Amazonの自律AIコーディングツールKiroがAWS環境全体を削除した後に再生成する事故を起こし、13時間の障害をもたらしている。
Amazonの対応はシニアエンジニアのサインオフを義務化することだった。だが同時にAmazonはAIコード使用率80%目標を維持し、3万人規模のリストラを進めていた。AIコードの監視を強化しながらAIコードの使用を拡大する。この矛盾は、いまの技術産業全体の縮図である。
ホーアが1965年に語った言葉を再読しよう。
「実装があまりに簡単だったので、誘惑を断りきれませんでした。」
そして2026年の現実:
「AIがあまりに簡単にコードを生成するので、誘惑を断りきれない。」
60年の間隔を置いて同じパターンが反復されている。短期の利便性が長期の安全性を打ち負かす誘惑。 ホーアはこの誘惑の構造を誰よりもよく知っていた。自身が一度かかったことがあるからだ。
バイブコーディング時代のデータ
勘ではなく数値で見よう。
CodeRabbitの分析によれば、AIが生成したコードは人間が書いたコードより1.7倍多くの問題を発生させる。Veracodeのレポートは、AI生成コードの45%がセキュリティ検査に失敗すると明らかにした。METRの研究はさらに驚くべきものだ。経験あるデベロッパーですらAIを使うと19%遅くなるという結果が出た。ツールが生産性を高めるという直観の真逆だ。
オープンソースコミュニティの反応はさらに直截的だ。Redox OS、Gentoo、NetBSD、postmarketOSはAI生成コードを禁止する方針を採択した。Debianは「決めないと決めた」という奇妙な立場を取った。Hacker Newsでは「AI生成コメント禁止」の投稿が2,748ポイントで1位に上った。
Tailwind CSSの事例はAI時代の逆説をよく示す。AIコーディングツールが直接コードを生成することで公式ドキュメントを参照するトラフィックが40%下落し、収益は80%急減した。AIが学習した知識の源そのものが経済的に持続不能になる構造的問題だ。
これらすべてのデータが示す方向は一つだ。「簡単だから」という理由で検証なしにコードを受け入れれば、その代価は必ず返ってくる。ホーアがnullで10億ドルを支払ったように。
AI時代にHoareの遺産がより重要になる理由
逆説的に、AIがコードを大量生産する時代に、ホーアの形式検証哲学がこれまで以上に切実に必要とされている。
Martin Kleppmannは**“Vericoding”**という概念を提案した。AIがコードを生成し、形式検証ツールがそのコードの正しさを数学的に証明する方式だ。人間がすべきことは「何を望むか」を仕様(specification)として書き下すことだけである。
これはホーアが1969年に提案したHoare Logicの現代的実現である。{P} C {Q} — 事前条件と事後条件を明示すれば、プログラムの正しさを自動的に検証できる。
実際2025~2026年の間にAIと形式検証の融合は急速に進んでいる。Dafnyを用いた自動検証率は68%から96%へと上がった。AIがコードを生成する速度と、形式検証がコードを検証する厳密さが結合すれば、ホーアが夢見た「欠陥が明白に存在しない」ソフトウェアに一歩近づける。
ホーアの格言を再び借りるなら:
- バイブコーディング = 「明白な欠陥がない」ほど複雑に作ること
- Vericoding = 「欠陥が明白に存在しない」ほど単純に作ること
AIがコードを書く時代、人間の役割はコードをタイプすることではなく、何が正しいかを定義することへ移る。これこそホーアが半世紀にわたって主張してきた、まさにそのことである。
追悼:「彼は正しかった、ただ生まれるのが早すぎただけだ」
2026年3月5日、トニー・ホーアが91歳でこの世を去った。
Hacker Newsに上がったある一文のコメントが彼の生涯を最もよく要約している。
“He was right, just too early.”
ホーアは正しかった。単純さこそ信頼性だと言ったとき、業界は機能を増やすのに忙しかった。形式検証が必要だと言ったとき、業界はテストカバレッジさえ上げれば済むと答えた。nullは過ちだったと告白したとき、世界はすでにNullPointerExceptionの上に積み上げたシステムで動いていた。
彼は正しかった。ただ世界が彼の言葉を理解するまでに数十年かかっただけだ。
ホーアとダイクストラ(Dijkstra)の友情は伝説的だ。ダイクストラが臨終を控えて書類を整理していたとき、先輩教授が数十年積み重なった書簡をどうするか尋ねた。ダイクストラの答えはこうだった。
「Tonyとの手紙だけ残せ、残りはすべて捨ててくれ。」
その教授自身の手紙も含めて。二人が生涯をかけて交わした知的対話の重みがどのようなものだったかを物語る逸話である。
ホーアは92歳近くまで”pinpoint sharp”な記憶力を保っていたという。ケンブリッジのArts Picturehouseでこっそり映画を観ていた老学者。60年前の自身の過ちを数万人の前で告白する勇気を持った人。アルゴリズム一つで世界中のコンピュータの速度を変えた人。
“Inside every large program is a small program struggling to get out.”
AIがますます大きく複雑なコードを吐き出すこの時代、ホーアのこの最後の格言は警告であり羅針盤でもある。複雑さの中から単純さを見出すこと。簡単なものに誘惑されず正しいものを選ぶこと。それがTony Hoareが我々に遺した遺産である。
道具は強力になった。しかし道具を扱う判断力は依然として人間の役目である。
Tony Hoare, 1934–2026. Rest in peace.