>>912
Haskellで証明が可能な場合が多いのではなく、すべての関数について証明をすることができる。
もちろん非常に難しいものもあるが。
再帰関数は証明が簡単である事が多いという事実もある。

>>908
形式的な証明は常に必要な訳ではない。今すぐ使いたいシステムで、多少のバグは許容される場合は、
形式手法は向いていない。
しかし、不具合が許されないシステム開発においては、テスト行程に莫大な予算がかかってしまう。
　[参考] UFJ銀行のシステム統合↓
http://itpro.nikkeibp.co.jp/article/OPINION/20080423/299886/
これは、システム開発にCOBOLやJavaなどを使っているためである。