とりあえず自分の立場を明確にしておきます。
今年の3月まで情報理工学研究科の修士課程でCS系の研究をしていました。
4月からは組み込み系の会社にエンジニアとして入社し、研修中の身です。未だに学生気分が抜け切らず、休日に積み論文を崩したりしています。
プログラムの検証とか証明の機械化とかその辺の研究をしていました。具体的にはCoqという証明アシスタントのUIというか言語の話ですね。
証明アシスタントのソフトウェア開発への活用例は現状ごく少数しか存在しません。（特にプログラミング未経験の人に）所属研究室の説明をするとき、言語処理系の改良などもひっくるめて「プログラマのためのプログラムを作っています」という言い方を個人的によくするのですが、そういう意味では未だ「プログラマのため」の段階にも至ってないかもしれません。
研究室は割と自由にやらせてくれるところで、研究室内でも割とテーマがバラバラだったりしていました。ので、結構ニッチをマイペースにやっていた自覚があります。
「最低でも一度くらいは対外発表しよう」という研究室の方針[1]はあって、実際発表はしてはいるものの、分野事情を知っていると胸を張って言うことはできません。分野の俯瞰や人の名前を覚えることはあまり無かった気がします。
アドベントカレンダーに参加した感想というかなんというか。
個人的にこのACは多分野が入り乱れる状態になるのが一番面白いと思っているので、なるべく前提知識を減らそうと心がけて書きました。リンクをたくさん張るとか脚注で補足するとか。
とはいえ説明慣れしていないこと、参加者を見る限り割とプログラミングの話が通じそうだったことから、C言語経験は前提としました。まあ最初に明示したので自分としては許してもいいかなと。
Asciidocが使えること、既にアカウント登録済みだったことからGistを使いました。
まあ媒体なんて別になんでもいいと思うんですが、残念なところがありました。割と脚注を使っているのですが、Gistでは（はてな等と違って）ツールチップとして浮かんでくれないので、脚注まで読んでくれる人はページ末尾と本文を行き来する必要があったのではないかと思います。これはAsciidoctorの問題なのでGistが悪いというわけでもないのですが。
他にも画像の追加が面倒な上に見栄えが悪いというのもあり、やはりちゃんとブログを使うべきだったのかなとは思います。一方で編集履歴が残って、かつ過去版を他人に簡単に見せられるというのはさすがGistという感じで、活用させてもらいました。
今回参加した動機は、前回（2016）のリベンジだったわけですが、そもそもなんで前回参加したかというと、読む側として「面白い企画なのに参加者少なくて勿体無いので賑やかしになろう」という想いからでした。その動機から初日をとりたくて、しかし見つけたのが11月末だったので時間が取れなくて苦しみましたが。
結局前回はその後人が増えることもなく悔しい思いをしたような記憶がありますが、今回はその辺あんまり気にしてなかったです。初日をとった意味はあったのでしょうか。
論文について
以下の記述については、全体的にあまり自信が無いです。
当然ながらプログラムにバグなんてあってほしくないわけですが、世の中ではプログラムの正しさというのは「試しに動かしてみて問題無さそうならOK」という方法で確認しています。これに対して、もっと厳密に正しさを追求するのがプログラム検証です。
検証したい「正しさ」を定める時点で大変だったりするのであまり実用例は多くないですが、特にバグの許されない分野では使われているようです[3]。
プログラム検証の分野では、例えば以下のようなジャンル[4]があります。
- モデル検査
-
プログラムの働きを簡単に示すモデルと呼ばれる表現[5]を作り、それに対して検査を行います。モデルはプログラムの設計図のようなものなので、先にモデルを作ってそれを基にプログラムを作る、ということもあるようです。
- シンボリック実行
-
実行時に決まる値を不定のまま、実行の様子を追っていく手法です。例えば、乱数で得られる値は不明なのでとりあえずxとしておいて、x<3という条件でプログラムが分岐したら「xが3未満の世界」と「xが3以上の世界」に分岐する、といった感じで、どんどん条件付きの平行世界が生み出される様子をイメージしてもらえればいいかと。
- 定理証明
-
式変形や帰納法などを用いて、数学の証明のようにプログラムを検証する手法です。一般に、普通の（数学の）定理証明も行えるようなシステムになります。人間がヒントを随時与えるITP（対話的証明器、証明アシスタント）と、全て自動で行うATP（自動証明器）があります。
私の専門はITPなので断言できませんが、この研究はATP+シンボリック実行という感じでしょうか。
この手法は何と言っても多言語対応という点が強みになります。正確に言えば、「Kで意味論が定義されている言語に対して」「検証したいプログラムと仕様を書くだけで」「十分な時間と計算資源さえあれば大抵の仕様を」検証できるということです。
検証器を作るために意味論定義を書くだけでいいというのは、かなり強みだと思います。プログラムを書く量が減るというのは、単に楽であるというだけでなく、バグが生まれ難くなるということでもあります。検証器なんてものを作る上では特に重要です。
論文では「意味論は既にあったから工数に入れなくていいよね」という感じでしたが、もし検証のためだけに意味論を書くとしたら、本当に楽になるのかはわかりません。ただ、どんな方法をとるにせよ検証器を作るのなら意味論を考えるのは特に重要な部分だと思うので、Kの学習コストさえ考えなければそれほど重くはない気がします。