昨日、某懇親会で天文関係者と話す機会があり、なぜか一瞬フォーマルメソッドの話に。情報工学ってのはほんとにサイエンスなのかい？*1ってな流れから。
否定的な意見も少なくないフォーマルメソッドについて、注目している理由を書いてみる。
それ動くの? に対する反論：CADのアナロジー
CADが産まれたはるか昔、その当時のコンピュータの能力を考えると「こんなもん使えん」と思う人が多数を占めたはず。でも、今やCADなしで世の中は成り立たない。
フォーマルメソッド関連の技術やツールも、現状だけで判断すると未来を見誤るのではないか。
経験だけでソフトウエアを組んでいる現代は確かにサイエンスでもエンジニアリングでもないが、きっと５０年先には普通にフォーマルメソッドでソフトを組んでいるはず。フォーマルメソッドやモデル検証は”ソフトウエアのCAD”と思っている。Computer Aided Software Design.
それ使えるの？ に対する反論：SQLのアナロジー
「SQLは"どのように計算するか"でなく"なにが欲しいか"を記述する新しい世代の言語」で「人間はコンピュータの動作を考えることなく、もっと上位レベルの何をしたいかだけ考えればよくなる」なんて宣伝文句があったらしい。
もちろん、こんなうまいことにはならず、現実は「SQLの動きを分析して、それをもとにコンピュータを速く動かすための方策を練る」必要がある。電子レンジでむらなくチンするために、ターンテーブル上での食品の置き方を緻密に計算するみたいな本末転倒にもみえる話。
しかし、世の中面白いものでこんなダメダメなSQLであるが、ますます使われるようになっている。理由は簡単でチューニングを施してでも使うメリットがあるから。それはDBを使って”完全なデータハンドリング”ができること。
フォーマルメソッドも、使うのが面倒なのは事実かもしれないし、将来も面倒なままかもしれないが、ひとつだけ確実なのは「フォーマルメソッドを用いて製造されたソフトウエアはバグがない」ということ*2。
よってバグがないことに価値が見出せるのならば、人は喜んで使うようになる*3。
で、今（2011.10.29 追記）
で、今、原発事故を経て「信頼性」だけでなく「安全性」の担保には何が必要なのか、いろいろ模索中。
*1:「情報科学でホントの理論はコンパイラだけだ」って話から「いや、分散アルゴリズムの理論はかなり進んだし、フォーマルメソッドもあるよ」と。しかしことフォーマルメソッドの中身はコンパイラと同じく計算理論だから話としてはおっしゃるとおりかも
*2:もちろん、仕様そのものに欠陥がある場合はどうしようもない。ただし仕様自体の穴も見つけけやすくなるのは確か。
*3:喜んでかどうかはコストメリットがあるかどうかというのも正論で、極端に面倒かつ時間がとられる場合は絶対に使われない。実際、「コストがかかりすぎてつかわれるようになぞならないだろう」という人も多い。ただ、現在でも製造期間の1/3が設計、1/3が実装、1/3がテストみたいな感じで設計に費す期間はそこそこ確保されている。なので、フォーマルメソッドを使うツールを導入するのもそれほど敷居が高いわけではないと感じている。
