流行

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