ウェンツェルの苦難の道
文書指向へと舵を切ったウェンツェルだが、まだまだ全然だし、先は長いし、苦難が予想される。
- 用語法、メンタルモデルがスクリプト指向のまま。
- ウェンツェル自身もfact, goalを多用している。
- 論理の概念・用語法と、ソフトウェアとしての証明系の用語・文化が違う。そこは強く意識すべきだ。
- 宣言的とは言っても、動作する証明系実装のメンタルモデルにより語っている。それを意識出来てない、自覚的ではない。
- Isar/VMって状態遷移モデルだしな。
- なぜに、証明図エディタにしなかった。
- バックワード推論だということを言ってないから分かりにくい。人間はフォーワードで考えることもある。
- 建前と本音の乖離状態。ポールソンの1990年マニュアルのほうが分かりやすい。
- ポールソンは本音で書いているが、ウェンツェルは建前に終始している感じが。
- 情報検索機能がとにかく貧弱。TeXとPDFにもオサラバして欲しい。
- コミュニティは長い歴史を持つからジャーゴンが形成されるのはしょうがないけど、多少は整理して欲しい。論理のためのボキャブラリーがどえらく非論理的。
- claim, theses, methodはIsabelle語。標準語（に近い言葉）で代替できなかったのか。
- context, premises, local factsもよくワカランし。
- goalのpremisesとか言うし、なにそれ。まー、ゴールをシーケントのように思えってことだろうが。
- goal, fact, methodはチャンと説明しないとダメだよ、ジャーゴンなんだから。
- term abbreviationsもジャーゴンだな。
- 用語assumptionのなんか独特な使い方があるみたいだが、説明されないとワカラン。
- print_ナントカ だの find_ナントカ のようなコマンドとしか言いようが無いキーワードをどうるのだ？ コンソールが出てないと意味ないし。
- thy_depsの実装はナンだよコレ。貧弱過ぎるだろう。
- GUIを全面に押し出すなら、ビジュアライズしないと。
- GUI vs TTY も、建前GUIだが、TTY文化があまりにも根強くて綻びだらけ。
- ツリーのノードと、そのノードからのサブツリーを区別しない事が多いが、これと似た事情の混乱が至るところにありそう。
- ノード一個しかないツリーもあるので、「ノードはツリーの特殊なもの」と言える。この種の言い回しも至るところにありそう。
