OCamlとかHaskellとか型はもう普通に流行っていてつまらない、と思う人へ。次のブームはモデル検査や定理証明だと思います。:-) エアバスの飛行機とか、Windowsのデバイスドライバとか、Javaカードとか、Cコンパイラとか、いろいろなものの「正しさ」が続々…