なんかヘン

• Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記

ウェンツェルの目標と志には全面的に賛同するが、なんか考えがとっちらかっている（一貫性がない、混乱している、中途半端）んじゃないの。

1. 宣言的文書がほんとにいいのか？
2. 自分の説明や論文では証明図使ってるじゃん。それが分かりやすいからでしょ。
3. なんで証明図をいちいちシリアライズせにゃならんの？ ちょっとアホくさいんですが。
4. Mizarに影響され過ぎでは。
5. もともとがシーケンシャルなコマンド言語なんだから、宣言的って無理がある。
6. 宣言部分をきれいに取り出しても、対話的に編集するのは別な困難がある。
7. 探索的・発見的なフェイズではコマンドを使い、清書するときに宣言的に書く、ってアドバイスがあったけど（Nipkowだったか？）、それオカシイでしょ。
8. 証明支援系じゃなくて、証明清書系になっちゃうよ。
9. コマンドインタプリタとしての対話性は悪いもんじゃない、むしろ活かすべき。
10. Unicode文字の扱いが無茶苦茶。
11. せっかくの斬新なアイディアも保守的思考に絡め取られている。
12. 30年もやっていたらしがらみはあるだろうね。キツイな、キビシイな。
13. Globularのような体験共有型ってのもあるし、それがないと教育には使えないと思う。
14. 時間性を排除したらダメだよ。人間は時間のなかで生きているんだから。