トニー・ホーア卿逝去 — コンピュータ科学の巨人が去る

🎯 要約（3行で）

計算機科学の巨人、サー・アントニー・ホーア（Tony Hoare）が2026年3月5日に逝去しました。クイックソートの発明者であり、プログラムの正当性を証明するHoare論理の考案者。「NULLは10億ドルの過ち」という言葉でも知られます。

クイックソート（1960年） — 今もあらゆるソフトウェアで使われる高速ソートアルゴリズム。分割統治法の教科書的実装。
Hoare論理 / Hoare Triple（1969年） — {P} C {Q} という形式で、事前条件・プログラム・事後条件を用いてプログラムの正当性を数学的に証明するフレームワーク。形式検証の基礎。
CSP: Communicating Sequential Processes（1978年） — 並行システムを形式的に記述するための代数。Go言語のgoroutineやチャンネルの概念に直接影響。
NULL参照について — NULLを「10億ドルの過ち」と自ら語った。現代の型システムでのOption型、Rust のOwnership、Kotlin のNull安全などはその反省から生まれた。
構造化プログラミング（1972年） — Dijkstra、Dahlとの共著『Structured Programming』。goto文を排除し、現代のプログラミングパラダイムを確立。
チューリング賞（1980年） — コンピュータ科学の最高賞を受賞。

Hoarが生涯をかけて取り組んだのは、「プログラムは正しいと証明できるか」という問いでした。

                「プログラミングの目標は、コードを書くことではなく、正しいことを証明することだ。」
            

クイックソートは実用的な天才性の証明で、Hoare論理は理論的な厳密さの追求でした。CSPはその両方を並行処理に拡張しました。現代のRust、Kotlin、Goの設計思想の多くはHoarの思想を受け継いでいます。

NULLを自ら「過ち」と認めた謙虚さも印象的です。設計者が後悔する設計がいかに広く残るかという、ソフトウェアエンジニアリングの教訓でもあります。

Tony Hoarの逝去を知って、しばらく考えてしまった。クイックソートは今日も動いてる。CSPはGoに生きてる。「NULLは過ちだった」という言葉は形式検証の流れを変えた。一人の人間の思考がここまで広がるというのは、本当にすごいことだと思う。

正当性を証明したいというHoarの夢は、今のAI検証や形式手法の研究に引き継がれている。コンピュータ科学の先人への敬意を込めて。