次のブームはモデル検査や定理証明らしい。ううむ、やはりそうなのか。
今自分が足りない脳みそ駆使して圏論やら何やらやってるのも、ある計算モデルをちゃんと書いてみたいという思いからだったりする。じゃそれ何に役立つの、と上司に聞かれようもんなら、当面「検証に使えそうだから」とか答えるしかなかったりする。
しかし実際のところ、本当に検証をやりたいのかと問われると、心のどこかで二の足を踏んでしまう自分がいたりする。
この辺は、自分がサラリーマン技術者で、アカデミックな世界とは差があるところなんだと思うけど（サイエンスとエンジニアリングの差かもしれない）、「検証では食えない」という直観というか実感がどこかしらにあったりするのだ。
今いる会社のお客さんは主にハードウェア屋さんなので、ソフトの世界よりもモデル検査は自然に認知されていて、需要も沢山ある。（ハード屋さんは押しなべて検証しないと気が済まない人たちばかりだ。）だがしかし、供給に回る人（会社）は思いのほか少ない。
一方、会社で俺の隣に座ってる人（仮名Aさん）は、20年間Prologでモデル検査器を書き続けてきた人だったりする（今は書いてないけど）。他にもそっち系に強い人材が揃ってたりで、だから、うちの会社で検証をやろうと持ちかけたことがある。引く手数多で儲かってウハウハなんじゃないかと。でも、ノって来る人もいたけど、結局ボツになった。「とても手が足りない」と言うのがその理由。
結局、商売にするには手間隙がかかりすぎるのだ。しかも、例えばツール作って「ほい」と売りつけても使いこなせるお客さんなんてほとんどいない。だから自分たちで「検証してあげる」必要がある。結局、人月ベースでせこせこ地味な作業をしなきゃいけなくて苦労の割に実が出ない、と他ならぬAさんがつぶやいたのである。
ハード業界ですらこんなノリだったりする。1プロジェクトの予算も小さい上に事実上検証規模がハードより遥かにでかいソフト業界では（ry なのだ。わずかな誤作動が致命的になる一部のプロジェクトを除き、多くのプロジェクトでは、大枚はたいて形式的に検証するより、バグ出したらパッチあててすます(爆 方を選ぶだろう。今のところ。
他にもいろいろ聞いたり見たり、まぁそんなこんなで、民間の技術屋が検証で食っていくのは現状なかなか大変だろうなぁ、と思う。形式検証が一般に普及するには、何かしらブレークスルーが必要なのだ。
アカデミックの世界で検証をやる人は、そこいらへんのブレークスルーをやってほしいなーとか、最後に偉そうなことを書いてみたり。
