λ計算では自然数やデータ型をも表現できるが，プログラムが常に意味のある結果になるとは限らない(行き詰まり状態．例えば true + 1 とは？)．式を実際に評価することなしに，プログラムの振る舞いをできる限り保証したいというのは自然な動機である． 項の…

定理証明支援系に興味を持ったが，特に証明したい定理があるとか数学に生かしたいといった目的はないので，仕組みを知るためにゼロから作ってみる．定理証明支援系といっても様々だが，ここでは主にCoqを念頭において話を進める．