証明支援系って、ほんとにマダマダ
マダマダというか、ダメダメというか。とっても使いにくい。30年間作り続けてこのレベルってことは、あと30年くらいはかかるのかな、生きてネーよ、チクショー。
次が欠けている。
- 情報検索機能
- アウトライン機能
- リソース管理機能
- ビジュアライズ機能
情報の提示がとにかく少ない、ショボい。ユーザーとの対話のバイド幅が狭い、というか。知りたいことが表示されてなかったり探せなかったり。頻繁に参照する情報はGUI上に見えてる必要があるが、それがないし、検索も検索後の閲覧も不便。
今挙げた4つの機能は相互に関係していて境界線も切りにくいのだが、実用上一番不便に感じるのはアウトライン機能の欠如。「文章を書くワープロはあるけど、構想を練るアウトラインプロセッサがない」感じ。文章を実際に書き下すより、アウトラインを考えるほうが重要なんだが、そこのサポートが全然ない。
ワープロの場合は、見出しだけを先に書き並べてアウトラインとするような使い方が出来る。が、今の証明支援系は、定理を書くと証明責務が発生するので、証明（責務のdischarge）をしないと先に進めない。証明のときはバックワードリーズニングだからトップダウンなのに、定理群の全体構成はボトムアップに固定される。
ボトムアップは探索的行為には向いてない。目標が先にあるのだから、まず目標を書いて、そのために必要な素材を考えていく。これがアウトライン構成、ないしは証明プラニングのフェーズ。プラニングは紙上で行って、出来上がってから証明支援系で書く感じ。これじゃ、支援系じゃないじゃん！ 証明清書系だ。
昔のワープロって、清書系で、原稿用紙にだいたい書いて写し取るとかしていた（のだろう）。もし、ワープロのバックスペースキーと上スクロールキーがないとしたら、精密な下書きがないと使えないだろう。今の証明支援系ってそんな感じ。
sorryコマンド（Isabelleの場合、CoqならAdmitted）で保留するとか、定理から公理に変えるとかは出来るけど、書き換え並べ替えが面倒！ 依存関係も可視化されてないし。
そもそも、証明支援系のUIとしてテキストベースがダメなんだと思う。セオリーの相互関係、定理の相互関係、証明図そのもの、いずれもグラフなので、グラフ編集とグラフ管理のソフトウェアになるべき。ウェンツェルの発想は、過去のプレーンテキストエディタからリッチテキストのワープロに進化させたいのだろうが、そうじゃなくてお絵かきソフト／ゲームソフトに向かうべき。テキスト表現が二次的なのは明らか。
定理やルールは、カードや付箋のようなメタファーで、関連するなら線を引き、種類が違うなら色を変える、とか。それを、クリックやドラッグ（今ならタッチ操作か？）で出来るようにする。エディタフレームワークjEditより、お絵描きやゲームのフレームワークを使うべきでしょ。
証明プラニング／アウトライン作成の機能が欠如しているので、タクティクス＝タクティクの集合はあるけど、ストラテジーは表現できない。「ビジュアルなストラテジーエディタ＝証明のアウトラインプロセッサ」が欲しい。
単一のセオリー内の定理の相互関係の把握もままならないのだから、複数のセオリー間の相互依存関係となるとホントに把握できない。現状、find, grep, lessでやる、ってレベル。原始的過ぎるだろ！ 人間がやったら退屈で大変な作業こそソフトウェアに支援して欲しいが、やってくれない。知的奴隷作業が人間側に押し付けられる。カンベンしてくれ。
情報検索機能とビジュアライズ機能が一体化した、セオリーブラウザ／インスペクタがあればいいんだが。現状は程遠い。
この30年間証明エンジンに注力してきて、UIは最近やっと、だから、致し方ない、とは言える。証明エンジンにしろ、ストラテジーエディタやセオリーブラウザが作りやすい構造をしてるわけではない。10年くらいで少しは変わるのかな? 30年は待ってられない、死ぬから。
