>>906
おお、こういうツールがやはりあるんですね。ありがとうございます。

Haskellというとコンパクトな記述とかがクローズアップされますけど、
参照透過性にこだわりを持つ言語ということで、テストではなくて
証明が可能な場合が多い、というのは刺激的だと思います。

>>908
テストと証明では質的な違いがありますよね。テストはどこまで行っても
信頼できる「と思われる」の積み重ねであって、絶対に間違いがあっては
いけないシステムの場合、テストは凄いコストかかるんじゃないでしょうか。

証明可能で、しかもツールでそれが検証できれば凄いコストが減らせます。
一般的な実用化を進めるに際して、重要な要素だと思います。