>>891
>>895
Haskellの関数と仕様を与えて、関数がその仕様をみたすことの証明をする支援ツールがある。
名前はAgda

このツールによって証明された関数は、仕様を満たすことが保証されるので、テストが必要ない。
このようなツールは証明支援系(Proof Assistant)、定理証明系(Theorem Prover)などと呼ばれている。