ハクソク

世界を動かす技術を、日本語で。

トニー・ホア氏が亡くなりました

77日前原文(lefenetrou.blogspot.com)

概要

Tony Hoare の訃報が Jonathan Bowen から伝えられた Hoareは 構造化プログラミング や CSP などで著名 彼の著作は多くの技術者に影響を与えた 関連資料や 口述歴史 も多数存在 本記事ではHoareの業績と影響を概説

Tony Hoareの訃報とその影響

  • Tony Hoare （C. A. R. Hoare）の訃報、 2024年3月5日 にJonathan Bowenより伝達
  • Hoareは 計算機科学の巨匠 として知られる存在
  • 代表作『 Structured Programming』（Dahl, Dijkstra, Hoare共著、1972年刊行）
    • プログラミング構造化の基礎理論を確立
  • 代表作『 Communicating Sequential Processes (CSP)』（1985年刊行）
    • 並行計算・プロセス間通信の理論を提唱
    • オンラインで PDF形式 でも閲覧可能（http://www.usingcsp.com/）
  • Hoareの理論は 現代ソフトウェア工学 の基盤
    • 安全性、正当性、並行性の分野で多大な影響

関連資料とさらなる情報

  • Jonathan Bowen による「 Oral History of Sir Antony Hoare」が公開
  • FACS FACTS 2024 誌にもHoareに関する記事掲載
    • 執筆者: T Denvir, J He, CB Jones, AW Roscoe, J Stoy, B Sufrin, JP Bowen
    • 論文タイトル：「 FACTS T Denvir, J He, CB Jones, AW Roscoe, J Stoy, B Sufrin, JP BowenFACS FACTS 2024 (2), 5-42」
  • これら資料は Hoareの思想と業績 をより深く理解するための重要なリソース

Tony Hoareの主な業績とその意義

  • 構造化プログラミング の普及
    • プログラムの可読性・保守性向上
  • CSP理論 による並行システム設計の礎
    • プロセス間の安全な通信モデル確立
  • 形式手法 への多大な貢献
    • プログラム検証や仕様記述の厳密化
  • 教育・啓蒙活動 も積極的に実施
    • 多くの研究者・技術者に影響を与えた指導者

まとめ

  • Tony Hoare は計算機科学の発展に不可欠な存在
  • 彼の著作や理論は今なお 世界中の技術者 に受け継がれている
  • 関連資料を通じて Hoareの功績 を再認識する意義

Hackerたちの意見

もし私がバカだったらごめん、何か見逃した？トニー・ホアは亡くなったの？どこにもニュースが見当たらないんだけど。

└

ブログの著者がジョナサン・ボウエンから聞いたって言ってるから、まだ公式には発表されてない可能性もあるね。

└

私もニュースを見つけられないけど、これが投稿の主張だね。 > ジョナサン・ボウエンが、トニー・ホアが3月5日木曜日に亡くなったと教えてくれた。（フランス語から翻訳）驚くべき理由は、そこからもう4日経ってるのに、このページ以外に何も発表されてないことだね。

└

それが投稿の主張だね。他では確認できないな。

└

うん。彼は先週亡くなったよ。

└

彼のウィキペディアのページはまだ現在形で書かれてるね。こういうのはみんなすぐに反応するから、まだ生きてるのかも？

└

残念ながら、それは本当のようだね。先週の遅い時間に、知っている立場の同僚から聞いたよ。

ビリー・クリスタルの後のスタンドアップのネタの一つで、彼の両親が友達と遊ぶ時の好きなゲームが「誰が死んだか当ててみて」って話してたのを思い出す。ここ数年、そのネタをよく考えてる。

くそ、トニー・ホアは、私が死ぬ前に会いたかった人のリストに入ってたんだ。大学院の指導教官が彼のことをすごく高く評価してて、確認できないけど、ホアが彼の博士課程の指導教官だったと思う。ホアの重要性は計り知れないよ。CSPやホア論理、UTPはそれぞれ独立した分野だからね。彼がいなくなったのは悲しいな。

└

彼に会ったとき、残念ながら彼がどれだけ重要な人か気づかなかったんだ（1987年）。私が働いていた場所では、FPUの設計を検証するために形式的手法を使っていて、PRGと協力してたんだ。確か、プロジェクトは成功したと思う。TLA+が出てくるまで、形式的手法が成功裏に使われた話は聞いたことがなかったな。

└

彼の情報は数学系系譜プロジェクトでいつでもチェックできるよ：https://mathgenealogy.org/id.php?id=45760

彼の仕事の多くが、適切な同期コミュニケーションチャネルを使って混乱を避けるシステムを作ることにあったことを考えると、この混乱はある意味適切かもしれないね。ヌルポインタの話は有名だけど、オッカムやコミュニケーティング・シーケンシャル・プロセスの研究が素晴らしかった。アクターモデルの人たちが反論するかもしれないけど、やっぱり素晴らしいと思う。彼の好きな名言は「ソフトウェアを構築する方法は二つある。一つは、明らかにエラーがないほどシンプルに作ること、もう一つは、明らかにエラーがないほど複雑に作ること。」これが本当でないことを願うけど、もし本当なら、非常にふさわしいご冥福を。

└

CSPとホーア論理は素晴らしかった。彼は形式手法の大きな支持者だったよね。彼は形式手法を主流にするのを諦めたけど、私はすぐに復活すると思ってる。生成されたコードに関しては、検証がボトルネックだね。彼は正しかったけど、ちょっと早すぎた。

└

そして、私たちはその素晴らしさを非同期の悪夢で無駄にしている。ソフトウェアはもっとシンプルでエレガントになれるはずなんだ。

└

アクターモデルも素晴らしく間違っているかもしれない。小さな正しいシステムを大きな正しいシステムに組み合わせることができないからね。（ソフトウェアの）トランザクショナルメモリやデータベースに触発された他のアイデアは、これに対してはずっと良い可能性がある。

彼（と他の多くの人たち）のソフトウェアの広範な形式検証の夢が実現しなかったのは悲しい。彼はコンピュータサイエンスに本当に根本的な貢献をしたけど、クイックソートや「10億ドルの間違い」に関する引用で主に知られることになるんだろうな。数十年にわたる形式手法をより扱いやすくするためのプログラムはあまり知られないだろう。ダイクストラが最短経路アルゴリズムだけで覚えられることを恐れていたという逸話を思い出す。

└

ソフトウェアにおける並行性管理に関する最初の引用された作品のほとんどは、C A R 'トニー' ホーアによって書かれたものだよ。彼がクイックソートを作ったことを、普通に忘れちゃうんだよね。

└

実は、AIのおかげで、これがすぐに変わるかもしれないね！広範な形式的検証がついに可能になる時代が来るかも。

トニー・ホーア卿は25年前にモスクワのシステムプログラミング研究所を訪れ、講演をしてくれた。自分の分野の生きた伝説を見られたのは忘れられない経験だった。彼はその時すでにシニアな人だったし、今日は彼の長く素晴らしい人生を祝うつもりだよ。

ティーンエイジャーの頃にトニー・ホアのカジュアルな講義を見たことがあるんだ。雰囲気は温かくて歓迎してくれる感じで、内容を全部理解してたわけじゃないけど楽しかった。彼はすごく優しくて、私の簡単な質問にも丁寧に答えてくれたのを覚えてる。

トニー・ホアに初めて出会ったのは、約24年前にカーニハンとリッチーの『Cプログラミング言語』を学んでいるときだった。長い間、彼のことをC. A. R. ホアとしてしか知らなかったんだ。インターネットに入ってから、みんながトニー・ホアって言ってるのが、私が知ってたC. A. R. ホアのことだと気づくのにちょっと時間がかかった。書籍からの関連する引用を紹介するね：> 再帰のもう一つの良い例はクイックソートで、これはC.A.R. ホアが1962年に開発したソートアルゴリズムだ。配列が与えられると、一つの要素が選ばれ、他の要素は二つの部分集合に分けられる - 分割要素より小さいものと、大きいか等しいものに。次に、同じプロセスが再帰的に二つの部分集合に適用される。部分集合に要素が二つ未満のとき、ソートは必要ない；これで再帰が止まる。> 私たちのクイックソートのバージョンは、最速ではないけど、最もシンプルなものの一つだ。各サブ配列の中央の要素を使って分割する。[...] これは私が独自に実装を学んだ最初の「真剣な」アルゴリズムの一つだった。もっと一般的に言うと、この本は私の人生に深い影響を与えた。コンピュータプログラミングに恋をさせてくれて、最終的にはそれをキャリアに選ぶことになった。K&R、トニー・ホア、そして私が立っている多くの巨人たちに感謝だ。

ここでの議論のほとんどはクイックソートとヌル参照のミスに集中しているけど、彼のコミュニケーティング・シーケンシャル・プロセス（CSP）に関する研究は、現代の並行および分散システム設計の理論的基盤を築いたんだ。ホア論理も、彼が最初に発表してから数十年経ってようやく広く使われ始めた形式的検証作業の基盤を作った。日常的なコーディング、アルゴリズム設計、そしてコアシステムアーキテクチャにこのレベルで影響を与えたコンピュータ科学者はほとんどいないよ。

この投稿はHNのフロントページから隠されてるみたいだね？