皆さん、ありがとうございます。

自分は手続き型しか経験が無かったので、プログラムが意図した動きを
するかをテストするという発想はあっても、証明するという発想はありません
でした。

それが、Haskell本ではよく出てくるので、アプリケーションの信頼性を「証明」
するということが重要なのかな、と思ったのです。

別にそんなこと一々しないんですかね。或いは、ツールで検証できたりする
んでしょうか。