形式手法 -- 次の30年

昨日Springerで買ったのは「形式手法 -- 次の30年 ( Formal Methods – The Next 30 Years) 」という今年10月に行われた国際学会の論文集だった。

冒頭の招待講演の内容にすこしゲンナリする。

形式手法は安全性を「証明」するだけでなく、安全性を改善するためにも用いなければならないという。まあ、それはいいのだが、学部の一年生から正規表現と有限状態マシンのことをきちんと教えるのがいいという話で話を締めくくっている。

「そこじゃないだろう。エライ人かもしれないが、話はピンボケ。」

生意気な自分の院生時代のことを思い出した。ピンボケと言われるのは、今度は自分の番なのに。

気を取り直して、次の論文「形式手法における人間」を読む。

この論文の主要な関心は、どうやったら仕様を書くことを人に教えられるのかということ。教育の問題に対する目配りは、広い。また、どうしたらそうした層を、子供からリタイアした人にまで、広げられるのかという「形式手法の民主化」という問題意識はいいなと思う。

次の論文は、形式手法で検証済みのマイクロカーネル seL4 を作ったアンドロニックのもの。彼は形式手法の受容の基本的問題を「アカデミックな研究」と「IT業界の実践」のギャップと捉えている。そうした分裂を克服した "One Team"の必要について、seL4開発の経験を交えて語る。それは、突き詰めれば「社会的要因」の問題だとする。

ここまでは良かった。

ただ、この二つの論文以降は、ずーっと、技術的な論文が並ぶ。どこにも「形式手法 -- 次の30年」の話はない。

だまされたみたい。

冷静に考えれば、若手だろうがベテランだろうが、「形式手法 -- 次の30年」なんてテーマの論文を「学会誌」に投稿しても、絶対、受理されるされるわけないんだから。「学会」の「表現」は「不自由」なものだ。

それに、「次の30年」って、長すぎると今気がついた。

僕だって、30年後のITを語ることはない。それは30年後の社会や、100年後の地球環境を語るより多分難しい。僕の視界は、長くて 10年か20年（適当に言っている）。

タイトルに、釣られたんだと悟る。

二つの論文のために、一万数千円はらったことになる。まだ、24時間経っていないので、クーリング・オフできないかな。

=====================
2019年11月20日  FBの投稿から