コンピュータの大型化、大容量化が始まった1960年代初期より、プログラミング言語の定義と設計に関するホーア論理の提唱をはじめ、プログラムの仕様記述、設計、実行、メンテナンスについて、コンピュータの性能を引き出し、ソフトウェアの信頼性向上のための公理論的アプローチに基づく種々の提案を行い、ソフトウェア科学の発展に多大な貢献をした。
Structured Programming, Academic Press, 1972
Essays in Computing Science, Prentice Hall, 1989
Quicksort. Computer Journal 5 (1), 1962
An axiomatic basis for computer programming. Communications of the ACM Vol.12, 1969
An axiomatic definition of the programming language PASCAL. Acta Informatica 2 (4), 1973
An operating system structuring concept. Communications of the ACM 17 (10), 1974
Communicating sequential processes. Communications of the ACM 2 (18), 1978
Programs are predicates. ICOT Journal 38, 1993
ホーア教授は、1960年代初期より、ソフトウェアの信頼性向上のために公理論的アプローチを中心に種々の提案を行い、ソフトウェア科学の発展に根幹的な貢献をした。
教授は1960年代初め、今日最もよく使われる効率の良い整列アルゴリズムである「クイック・ソート」を考案した。これは、その基本アルゴリズムを簡潔な再帰的記述によって表現する画期的なもので、当時の計算機の性能を最大限に使った高速で巧妙な手法であった。
1969年、教授はまた、ホーア論理と呼ばれている公理論的意味論を用いて、プログラミング言語の定義付けと設計を行った。これは、教授の深い洞察力と独創性に裏打ちされ、それまでのソフトウェアの歴史に一線を画す強力かつ優美なものである。ここに、教授はプログラミングを厳密な科学として確立した。1960年代後半、コンピュータの大型化、大容量化に伴い、大規模ソフトウェアの開発が要求される中、その開発の困難や、システムの信頼性の問題からソフトウェア危機が叫ばれたとき、教授はホーア論理を基礎に、プログラムの正しさは論理的に検証されるべきものであるとの指針を明確に打ち出した。
ここで教授は、構築されたソフトウェアの正当性、信頼性を保証するための方法論を与えるべく、データ型の概念を明確にし、データの構造化の重要性を主張するとともに、階層化と抽象化を中心に据え、プログラムを段階的に詳細化していく構造化プログラミングの体系を提唱した。この教授のデータ型の概念と検証規則は、良質なプログラム設計のための根本的な指針となり、ソフトウェア危機を克服するための大きな原動力になった。また、1972年には、オペレーティング・システムの抽象化と構造化の研究を通じてモニターという概念を提案、さらに、その後提唱された並列処理システムの挙動を記述する理論的枠組みである相互通信逐時システム(CSP)は、並列コンピュータの実用化に基礎を与え、今日の普及に大きく寄与した。
ホーア教授のソフトウェア科学に対する業績は、いずれもが高度化、多様化するコンピュータソフトウェアの根幹にかかわるもので、分野の広さ、またその理論の深さのすべてにおいても比類のないものであり、安全な情報化社会を構築するために不可欠な技術的基盤を与えるものであった。今日のソフトウェアにかかわる科学と技術の発展は、教授の業績に負うところがきわめて大きい。
よって、ホーア教授に先端技術部門における2000年京都賞を贈呈する。
私は興味深い時代に生きてきました。本日は、情報科学者としての私の考え方、キャリアを決定付けた運命のめぐり合わせ、ならびに周囲の状況についてお話しさせていただきます。私の犯した過ちから学び、あるいは成功談に勇気づけられ、「人のため、世のために尽す」という京都賞創設者の理念の実現に向けて努力してみようと考えられる方がこの中から何人かでも出てくだされば幸いです。また、そうなることが、第16回京都賞を授かったことに対する何よりの恩返しとなるのではないかと思います。
私は1934年にスリランカで生を受けました。第二次世界大戦中は、ジンバブエと南アフリカで何年か過ごしました。1946年、父がイギリスに引きこもったのを機に、私も遅れ馳せながら伝統的な英国式教育を受けることになりました。古典ギリシャ文学、ラテン文学、ならびに両言語学を専攻した私は、1956年にオックスフォード大学を卒業しました。在学中には、古代史や、以前から好きだった哲学の勉強もしました。また、英国海軍で2年の兵役を務める間に、ロシア語を学びました。その後、大学院生としてオックスフォードに戻り、統計学の課程を修了しましたが、専門分野に関する公式の資格としては、これが唯一のものとなります。私が統計学に魅せられたのは、それが人間の知識や不確実性に関する哲学的な問いと関わりがあるように思えたからです。学生生活の最後の年は、モスクワ国立大学でコルモゴロフ派の確率の研究を行っていました。そこで私はクイックソート・アルゴリズムを発明し、コンピュータによる自然言語翻訳の最先端の研究に関わりました。こうした研究をテーマに、私は、最初の学術論文をロシア語で執筆、出版しました。
1960年、イギリスに戻った私は、研究生活に終止符を打ち、就職することにしました。就職先に選んだのは、小さなコンピュータ・メーカーで、私はプログラマーとして採用されました。実を言うと、当時、私は、コンピューティングの進歩は、すでにピークを過ぎていたと考えていたのですが(大きな間違いでした)、この会社で、またしてもコンピューティングという学問に見え隠れする哲学との関わりにすっかり魅せられてしまったのです。この会社では、人工言語である国際的算法言語ALGOL60用のトランスレータープログラムの開発を担当しました。その後、実力以上の昇進を果たした私は、OSの開発責任者に任命されましたが、こちらはうまくいかず、また、機械アーキテクチャの開発も行いましたが、こちらも成功しませんでした。後に、この会社が2度にわたって、より大きな会社に吸収されたために、私はベルファストにあるクイーンズ大学のコンピュータ科学教授として再び大学に戻り、8年間の宮仕えで培ったコンピューティングに関する知識の講義を行うことになったのです。
私がベルファストに赴いた1968年当時は、ちょうど北アイルランドの社会情勢が不穏化し始めた頃でした。ほんの最近まで一向に沈静化の兆しが見えなかったこの問題ですが、そうした時代背景にもかかわらず、私は優秀な教授陣をコンピュータ学部に迎え入れることができ、急速に拡大しつつあったこの分野における教育の要求に応えることができたのです。当時の私は、民間で行った初期のプロジェクトの成功、あるいは失敗の理由を自分なりに解明することを研究の具体的目標としていました。こうした課題に取り組むにあたり、私は、長期的かつ、哲学的とでも呼べるようなアプローチを取ることにしました。私は、現役研究者としての以降のキャリア全体をカバーする研究予定を立てたのです。30年先に私が引退するまでには、研究の成果が、民間で実用化できるほどまとまったものとはならないだろうと考えたのです。1977年、コンピュータ学の教授としてオックスフォード大学に招かれた私は、またもや地道に資金集めを行って、教授陣をリクルートし、コンピュータ学を同大学のカリキュラムに取り入れるべく尽力しました。昨年、私は、同大学数学部上級教授の職を辞し、再び民間に身を投じることになりました。
現在、私は、ケンブリッジにあるマイクロソフト研究所に上級研究員として勤務しています。同研究所では、大型コンピュータソフトの開発者が、私をはじめとする理論研究者の研究成果を応用することによって、そのソフトを使う多くの人々が利益を得る、という若い頃の夢を追求しています。近い将来、こうした大型ソフトをまったく使わなくても済む人を捜すのは難しくなるでしょう。
Developing Powerful, yet Reliable Software Systems