ダメだなぁー
現状がこれでは、先が長くて気が遠くなる。
- 証明オブジェクトは人間が見ても意味不明（Coq）か、見えない（Isabelle）。
- リーズニングの記録としての証明スクリプト（＝タクティクの列）は、見てもわからない。
結局、見て分かるものが何もない。証明をする人と証明を知りたい人（読む人）との理解可能な伝達手段がないに等しい。手で書き直す必要がある。何のためのソフトウェアなんだか。
ウェンツェルがこの状況を改善しようといているのは分かる。が、Mizarをお手本にするのがいいのかな？ それだと、対話的ソフトウェアとしての出来は向上しないよな、Mizarは対話の対極にあるバッチ処理だから。
- 対話的ソフトウェアとしての使い勝手
- 論理的コミュニケーションの媒体、伝達の能力・効率
どちらも、情報の提示方法がキモだと思うのだが。
