高級指向もほどほどに

今のIsabelleに感じる違和感と難解さって、高級指向（高級志向じゃなくて、高水準言語指向）が過ぎるせいでは？ そんな気がした。

志、方向性（志向）としての高水準化、ドキュメント指向、宣言指向は否定しないが、まだ出来てないのに、ユーザーに押し付け過ぎだと思う。

• デフォルトではOutputパネルが出ない。
• Outputパネルを出しても、デフォルトでは証明状態が表示されない。
• 内部状態、コンテキストにGUIからアクセスできない。ショボい古いコマンドだけ。
• タクティクの説明がかなり後にならないと出てこない。
• 内部メカニズムの説明は意図的に避けているようだ。
• かといって、概念的・抽象的なモデルがキッチリしているとも言いがたい。

高級言語のコンパイラを使うのにアセンブラとハードウェアの知識は不要だ、というのと同じツモリだと思う。が、今のIsabelleは高級言語になれてなくて、マクロアセンブラのレベル。アセンブラとハードウェアの知識なしには使えない。だが、そこを隠そうとするから、わけわかんない。

論理だ証明だというけれど、所詮はコンピュータ上で動くソフトウェア、処理系だ。処理＝動作／手続きを完全に捨象するなんて出来ないし、実際出来てない。UIと説明が先走って低水準を隠蔽しても使えなくなるだけだろうよ。

ちょっと風変わりなプログラミング言語と割りきったほうがいい。論理系の実装というよりは、論理寄りのプログラミング言語だろう。だから、ランタイムの中身はこうなっていると理解したほうがいいと思う、少なくとも現時点では。