小林研究室への誘い
小林研究室の研究内容は何か？
一言で言ってしまえば，「ソフトウェアに関する基礎理論」，つまりソフトウェアを科学的対象とし，
その構成法，分析手法を研究するということです．具体的には，例えば
人間にわかりやすい言語で書かれたプログラムをコンピュータの言葉（機械語）
に翻訳する（コンパイル），ソフトウェアが期待通りの動作をすることを検証する，
あるプログラムをより高速なプログラムに変換する，といったことを，
ただの「職人芸」としてではなく，「科学的」に，緻密な理論のもとに行うと
いう研究です．（「もっと具体的にどんな研究があるの？」という人は
研究紹介のページをみてください．あるいは、研究室に来てもらえれば
プログラム検証ツールのデモなどもお見せできます．）
では
なぜ、ソフトウェアを科学的にとらえる必要があるのでしょうか？
なぜ
「職人芸」ではいけないのでしょうか？
現代の社会を見渡してみてください．飛行機や自動車の制御，医療器具，銀行
のオンラインシステム，原子力発電所，電子政府，今や世の中のあらゆるシス
テムがソフトウェアによって制御されていますよね．あなたは今のシステムを
本当に安心して使うことができますか？銀行のATMや証券取引所のダウン，コ
ンピュータウィルス，ロケットの墜落，医療器具の誤動作など，ソフトウェア
の欠陥に起因する問題は後を絶ちません．それは今のソフトウェア開発の現状
が「職人芸」の域を越えていないからではないでしょうか（実際には多くのソ
フトウェアシステムは「職人」の域にも達していないプログラマによって開発
されているという話もよく耳にします）．あるソフトウェアの開発現場では，
開発したソフトウェアを月曜日にテストし，火曜日にテストし，というように
各曜日ごとに検査するというのをまじめにやっているそうです．これって何か
ばかげていますよね？（もちろん、曜日に依存する部分があるのは確かなのですが，
きっともう少しまともな方法があるはずですよね？）
こんな現状を打破するためには，やはりソフトウェアをもっと科学的対象として
とらえ，緻密な理論のもとに開発・検証を行う必要があります．
ソフトウェアの理論って難しい？
小林研究室の論文を見ると素人にはよくわからない
記号がいっぱいならんでいます．
これらは，数学の方程式やベクトル，微積分の記号のように，プログラムの性質を
議論するための言葉であって，慣れれば難しくありません．
研究室に入って半年もすれば慣れます．
それどころか，小学校の鶴亀算が連立方程式をならうとすらすら解けるようになり，小中学校の
ひらめきを必要とする初等幾何（補助線を引いて解いたりする図形問題です）が
座標やベクトルを使うと機械的にとけたりするのと同じで，プログラムに
ついて分析するのにとっても便利な道具なのです．これらを使いこなせるか
どうかがただの「職人プログラマ」と「ソフトウェアの専門家」の差といって
いいかもしれません．
ソフトウェアの理論の研究のやりがいって？
ソフトウェアの理論というと，直接目に見えるものとして現れるのはプログラミング言語，
プログラム検証ツール，プログラム変換ツールなどです．ロボットが動いたり，
アニメーションが動いたり，っていう派手さはありません．でも，よく考えてみてください．
よいプログラミング言語，検証ツールを作れれば，飛行機や自動車，ロボット，
銀行や証券のオンラインシステム，医療器具など世の中のあらゆるシステムが恩恵を受けるのです．
表には出なくても，ソフトウェアの科学技術がコンピュータ社会を裏で支える
基盤技術となるのです．そんな、これからの社会を裏方で支える技術にあなたは興味がないですか？
ソフトウェアの「科学」としての面白さ
プログラミング言語や検証の研究は，工学的面白さだけでなく，科学的，理学的
な見地からも広がりと奥行きのある世界です．例えば，私自身，この世界に入って
はじめて知って驚きましたが，ソフトウェアの世界と（「AならばBが成り立ちかつAが
成り立つならばBが成り立つ」といった推論を体系化した）論理学の世界とに
実は密接なつながりがあるのです．また，世の中にはどんなに計算機が速くなっても
解けないという問題があるといったことも，ソフトウェア（というか計算）の理論を
展開すると見えてきます（これはたぶん学部で習いましたよね）．こういった，
ソフトウェアと論理学などの思わぬ学問のつながり，そしてそういったつながりから
見えてくる計算できない問題の存在など，数学やパズルが好きな人にとっては
きっと驚きわくわくするような世界がソフトウェアの科学には広がっているのです．
最後に...
上の短い文章ではまだピンとこないかもしれませんが，
上の文章を読んでちょっとでもソフトウェアの科学に惹かれた人，
現状のソフトウェアの欠陥の多さに日頃から憤慨している人，
これからの社会の基盤となる技術を研究したい人，数学やパズルが好きな人，
ぜひ小林研究室で一緒に研究しましょう．
（文責：小林直樹）
)まで