Scribble at 2026-03-10 09:19:49 Last modified: 2026-03-10 13:54:46

トニー（アントニー）・ホーアが亡くなったようだ。はじめて Hoare logic を知ったのは、何年前であったろうか。クリアな議論によってシンプルな公理系を展開した、いかにも古典的な業績にふさわしい論文は、もちろん "Papers We Love" でも取り上げられていたし、僕も当サイトで紹介したいと思っていた。実際、コンピュータ・サイエンスのプログラミング言語論においては、まさしく古典中の古典と言ってよい論文である。しかし、IT ベンチャー業界は言うに及ばず、コンピュータ・サイエンスという学界ですら、日本ではイノベーション馬鹿か守銭奴が大勢を占めており、こういう基礎研究に興味のない研究者や実務家や出版社が少ない状況では、「ホーア論理」を著作物の１章ていどで扱っている事例すら、ここ20年は見かけない。

また、オンラインでも「ホーア論理とは」みたいな note や Qiita のゴミ解説ばかりが散乱しているものの、幾つかの参考になるリソースは見つかる。まず、過信はできないがウィキペディアのエントリーがあるし、檜山正幸氏のブログでもたびたび取り上げられている。また Software Foundations という教科書シリーズを翻訳しているページにも多くの解説がある（ちなみに権利関係を明示していないから訝しいと思うかもしれないが、オリジナルのサイトでソース・コードの LICENSE というファイルに、翻訳も含めた二次利用を無制限に許可する旨が書いてある。なので、かつてあった経済学の海賊翻訳サイト・・・もう名前も忘れてしまったが「道草」だか「石清水」だか、軟弱右翼みたいな名称だった・・・などとはぜんぜん違うものだ）。