（Coqのような）証明系は正しい証明を記述したならば、それが正しいことを
必ず有限の時間で検証を終えて停止するのだろうか？
その有限の時間だといっても途方も無く長くなったりしないのだろうか？　
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか？
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか？

C言語とかAlgolのような普通のプログラミング言語は、
コンパイルすべきプログラムの長さNに対するコンパイル完了までの時間は
O（N log N)程度になってる。もしもコンパイルの時間がたとえばO(N^2)
かかるような言語とかコンパイラであると、プログラムの記述が大規模になれば
実用性が低くて使い物にならない感じになる。