いくつか関数型言語を使う企業を見たり、経験しているが証明はまずしない。
定理証明支援系で証明できることはどうせたかが知れており、
これは業種にもよるので断言できないが、実際に保証したいことはまず
証明できない。できたとしても時間かかりすぎ。仕様が変更されれば
証明に要した労力も無駄。費用対効果の面から魅力を感じられない。

自動、半自動的な検証は当然大いに利用したいが、モデル検査はちょっと
おおげさ。やはり言語に付属している型検査、型推論が妥当な手段になる。

企業側が関数型言語を選ぶのにはいくつか理由があるが、結構重要視されて
いるのが、関数型言語を書ける人間を集める方が、Javaで集めるより、
当たりが多いという事実。もちろんそういう意味では機械証明ができる人材は
歓迎される。まあ、面接や2chのスレを見てる限り、これももうすぐ成り立た
なくなるだろうけど。