引用

CoqでもIsabelleでも同じ。

Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記 :

• Coqシステムは、そして自分は、いったい何をやっているんだ？
• これが証明って、いったい何でだ？

こういう疑問を払拭できないのは、CoqのUIが貧弱なせいもあると思います。眼前の敵＝モンスター＝ゴールだけを表示するのは、バトルに没入するにはいいかも知れませんが、全般的な戦況が読めないのです。証明の現状を俯瞰的に眺めたいとか、出来上がった証明＝終わった戦いを（時系列ではなくて）構造的に視覚化したいとかの要望に応える機能がありません。

しょうがないので、頭のなかに証明の状況や構造を描こうと思うのですが、それに対するモデル＝考え方の基準がなんだか分からないのです。その結果、「何をやっているんだ？」「いったい何でだ？」とフラストレーションが募ります。