http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?Shiro

俺は静的型でバグが潰せるというのはまやかしの安心だと思っているが、静的検証ツールでバグが潰せるというのは信じている。

結局のところ現在の世の中で普通に利用されている型システムというのは,コードを書くときに楽,という程度の解析しかしてくれないわけで,非常に中途半端な存在であるとも言える.

中途半端,というか評価が難しい,というか.

筋のいいセマンティクスを選べば,完全だったり健全だったりする型システムを作ることはできるので,過去の型システムに対応するセマンティクスと比較することで,少なくとも定性的な評価はできる.が,しかし,現実の言語を考えてみれば,完全はおろか健全にすることも難しかったりするわけで,そうすると「それで何ができるようになったの?」と言われても,そう聞いてきた人を納得させられるなにか意味のある事を言うのは難しいし,ヘタをすると型システムを開発している本人すらよくわかってなかったりするのがオチ(俺)*1

私のいる界隈の分野で「何を言ってるんだかいまいちよくわからないけど,とりあえずすぐ使えて,それなりに便利」という製品を作ることができるんじゃないかと思うんだけど,優秀な人はもっと筋のいい(でもあまりすぐには役に立たない)問題を選んでうまいこと論文を書いていくのだろうし,私にしても来年以降はまじめに問題を考えるようにしないと,「単位取得退学」どころか(進学が決まっている専攻では単位を取得する必要がないので)単位を一個もとってない「タダの中退」になってしまうことになるので,結局「まあいつか気が向いたらやることにしよう」となって,そのままお蔵入りになるんじゃないかと思う.

*1:本人すら〜は特異例,というか冗談