プログラムというものは思い通りに動くのが当然、と思いがちですが、実際にはなかなか思い通りに動いてくれません。予想通りに動かない場合は、プログラムに間違いがあるはずです。間違いがないかどうか確かめるのは簡単、試しに動かしてみればいい、と思われるかもしれません。しかし、実はそれはとても難しい。
たとえば会社の事務仕事のプログラムのテストを考えましょう。プログラムに入力するかもしれないデータが何億何兆も無数にあることはすぐわかります。その全ての場合についてテストすることは実際には不可能です。一方、飛行機の制御ソフトウェアを考えてみると、実際に飛行機を飛ばして行うテストは、たとえ一回かぎりでも大変な労力がかかります。それを何億回も繰り返すなんてとてもできません。
テストにはいろいろ問題があるので、別の方法が考えられています。プログラムに何が書いてあるか、文面をよく分析し、「こう書いたプログラムはこう動くことになっている」という事実を積み重ねて、確かにプログラムが思い通りに動くかどうかを推論する方法です。プログラムが思い通りに動くことの「証明」をするわけです。

・プログラムとは何か？（算譜意味論）
・正しいプログラムとは？（算譜検証論）
・システムが妥当とは？（妥当性確認論）

これらが我々の研究室の基本的な問いです。プログラムを書くだけでなく、書いたプログラムが思い通りに動くかどうか検証することを考えます。このようなプログラムを書きたいという「思い」を厳密に書き下ろしたものは「仕様」と呼ばれます。仕様そのものが矛盾していたり、仕様が法律や倫理さらには危機管理などの多角的な要求を十分考慮していないために問題が起こる場合もあります。この場合は、プログラムがいくら仕様通りに動いても、やはり問題が起こってしまいますので、仕様の妥当性確認も必要です。このようなことを追究していくと、一般にプログラムはどんな性質をもっているのかという問題につきあたります。自分が書く、あるいは自分に関係のある特定のプログラムのことではなく、プログラムの一般論を考えることになっていくのです。こういうわけで、我々は、プログラム“で”研究するのではなく、プログラム“を”研究するのだ、といっています。
プログラムをどのようにして書くか（プログラミング）についても、我々は大きな関心をもっています。そもそも、仕様通りに動かないプログラムができないようなプログラムの書き方はないだろうか、という問題意識があります。
さらに、我々が最近研究しはじめたのがシステムの「人的要素」の部分です。ソフトウェアがうまく働くには、その運用や保守などの機械ではなく人間が操作する過程がうまく働く必要があります。このような過程を、プログラムが思い通りに動いていることを証明するテクニックを使って分析できるのではないかと考えています。さらに、企業や役所などの人間による組織も分析できないか、と考えることもあります。まあ、これはちょっとまだ思いつきの話ですけれど。たとえば企業はいろいろな法律や政令などのルール、業界のルール、自社が作ったルールなどに従って仕事をしています。こういうルールは、私たちの世界のプログラムと同じように見ることができそうです。プログラム分析の手法が、会社の経営分析にも適用できるのではないか、そんなことも夢想しています。

私は常々、真理そのものに向き合う態度を大切にしたい、と考えています。「偉い人がそう言っているから」あるいは「大勢の人がそう言うから」といったことは、ものごとが正しいかどうかの理由にはなりません。「千万人といえども我行かん」という気持ちを忘れず、他の人が何を言っているかとは別に、自分自身でものごとを確かめる態度を大切にしたい。
一方、ものごとを他人に伝えることは、真理を知ったり確かめたりすることとは別です。自分が知って確かめたことを、何でもかんでも他人に伝えるべきとは限らないようです。これは他人に話すべきことなのか、また、話すべきなのであれば、どのように話せばわかってもらえるか、ということに意を用いることも大切だと、最近気づき始めているところです。
これらは、自分でそうしたいと思いながら、なかなかできずにいることです。学生諸君と一緒に、このような態度を身に付けた人間になっていけるように努めていきたいと思っています。