絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。
ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。
証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。100%グラフィカルで、テキストによる表現や命令は一切使いません。パッと見ただけでは、何をするものか見当が付かないのではないでしょうか。
このソフトウェアを開発したのは、アブラムスキーとクック（この記事に二人の写真あり）が率いるオックスフォードのQuantum Groupで、開発の中心人物はジェイミー・ヴィカリー（Jamie Vicary）です。
Quantum Groupは、数年前から同種のソフトウェア（diagrammatic proof assistant）としてQuantomaticも提供しています。QuantomaticはMLとScalaで実装されたデスクトップ・アプリケーションです。
絵（diagram/picture）を使った証明支援系というククリでは同種ではありますが、GlobularとQuantomaticは、背景理論も実装方式も随分と違います。同種だけど別物です。Quantomaticは特に使いたいと思いませんでしたが、Globularには興味を惹かれました。
その事情は単純で、Globularによる描画が僕がいつも手描きで描いている絵（例えば「絵算の威力をお見せしよう」とかで描いているような絵）に近いので、お絵描きツールに使えそうな気がしたのです。
実際に使ってみると、Globularが描く絵は作業用で、人に見せる絵を描く能力はありませんでした。例えば、ワイヤーやドットの形状を変えることは出来ず、注釈としてテキストを書き込むことも出来ません。他にも不足している機能やバグがあり、使い勝手もマダマダな感じです。
しかし、高次圏論とストリング図をベースにしたソフトウェアが現に動いているという事実は素晴らしいと思います。Globularが存在することが、新しい認識／新しい問題意識／新しい課題／新しい世界観を生み出す契機になるかも知れません。
Globularの機能不足や使い勝手の悪さに文句をたれるのは容易ですが、ではどうしたらいいのかを提案するのは難題です。このテのソフトウェアを設計・実装することの困難さが身に沁みて分かります。
Globularを触ってみて、僕が深刻な問題だと感じたのはコミュニケーションの問題です。例えば、Globularのマニュアルを上手に書けるでしょうか？
テキストによるスクリプトは全く使わないので、何をするにも「あのボタンを押して、どこをクリックして」といった説明になります。ボタンやクリックに対する反応は、ソフトウェアの状態により変化します。画面の説明も「絵のこの部分は何の意味で、あっちはこう解釈して」となりますが、出現する絵は千差万別です。
Coqを使ったときも似た困難を感じました：「業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2）」より：
文章と図でCoqとの対話過程を見せることは大変です。Coqの解説を書いている人はみなさん苦慮されていると思います。
[...snip...]
これらの画面が時々刻々と変化していきます。画面キャプチャを大量に使うのも面倒だし鬱陶しい。ビデオ教材が有効かも知れませんが、それも手間。
Globularのマニュアルはあるにはありますが、これは内輪向け、つまり分かる人には分かるタグイのものです。チュートリアルは案の定ビデオ（YourTube動画）になっています。
典型的事例に沿って解説するチュートリアルならビデオ教材が使えるでしょうが、リファレンスマニュアルはどうしたものでしょう。リファレンスは通読するものではないので、目次や索引が重要です。目次項目／索引項目はテキストによる語（文字列）です。Globularにおけるトピック／サブジェクトは、「あの絵、この形、その行為」などです。テキスト表現が困難または不可能なのです。
テキストによる記述や命令が出来ないソフトウェアでも、日常的な直感を頼りに使えるならともかく、Globularは抽象的な理論をモデルとして動作します。
こうなると、Globularの使い方や背景を伝えるには、その場で面と向かって、疑問に答えたり、指さしながら説明したり、と、そんな行為が必要になりそうです。どんなソフトウェアであれ、その場で面と向かって教わる／教えるのが効果的ですが、Globularの場合、それ以外の手段ではだいぶ困難そうです。一子相伝とは言わないけど、いにしえの徒弟制度に戻れ、みたいな。
「その場で面と向かって」を要求しないコミュニケーション手段として人類は文字／活字を発明活用しました。インターネットが使える現代でも、テキストによるコミュニケーションは多くの場面でやはり有効です。しかし、テキストでは記述できないナニモノカを伝えるための、「その場で面と向かって」以外の手法はあるのでしょうか。
2次元以上の計算や証明を1次元テキストで行うのは無理があると思いますが、そうは言っても我々は、テキストでは記述できないナニモノカについてうまく語る手段をほとんど持ってません。
Globularは、我々のコミュニケーション形態に対する試練のように思えます。
[追記]Globularのサンプルをいくつか書いて公開しました。次のエントリーとそこからリンクされているエントリーにサンプルの記述があります。
[/追記]
