以前、証明支援系Coqの記事を書いたことがあります。今日話題にしたいIsabelle（イザベル）は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています（Coqもほぼ同時期にスタートしています）。十分に枯れた処理系でありながら、現在でも開発は活発で、新しい地平に向けて果敢な挑戦も試みられています。特に、ユーザーインターフェースの改善に熱心で、現在のGUIフロントエンドであるIsabelle/jEditには、驚くべき機能（の卵）が実装されています。
内容：
継続的チェッキング
理屈や背景は後回しにして、「継続的チェッキング」を簡単な実例で紹介します。
Isabelleは証明支援系ですが、プログラミング言語Standard ML（以下、SMLと略記）のコードエディタとしても使えます。7文字からなるSMLの式 val n=3 を、IsabelleシステムのGUIフロントエンドであるIsabelle/jEditで入力してみます。
赤いブロックがカーソル（キャレット）です。入力した式の評価結果が左側の出力パネルに表示されています。これだけ見ると、コンソールからSML処理系（Poly/MLといいます）を実行し、「コマンドラインとして入力して、コンソール出力を見る」(↓)のと同じように思えます。
いやいや、違うんです。ぜんぜっん違うのです。Isabelle/jEditは、コンソールによるRead-Eval-Printループとは、まったく違う対話的環境なんですよ。式の入力過程を1文字ずつ見ていきましょう。まず、'v'を入力したところ。
'v'だけではSMLの式になってないので、構文エラーが報告されています。それ以降も1文字入力するたびに、出力がめまぐるしく変わります。
そして、意味のある式 val n=3 が入力された瞬間に型推論と評価がされます。最初にお見せした画像の状況ですね(↓)。
「1文字入力ごとにテキストをインタプリタに渡してるだけじゃん」 -- まー、やっていることはそうなんですが、エディタとインタプリタ*1のあいだは、それ専用に設計された非同期プロトコルで通信して、コマンドラインごとの解析・評価ではなくて、ソースドキュメント全体での整合性が常に監視されています。
それを見るために、次の状態から始めましょう。
この状態で、カーソルを最初の行に移動して編集をします。すると：
関数値も再計算されています。関数の定義のほうを変更すると：
やはり、計算結果の値が変わりますね。
構文的／意味的エラーがあるかどうかをモニターするために、別パネルを出しておく必要はありません。証明ドキュメント内であれば、エディタの編集エリアの端っこ（ガター領域）にエラーのマーカーが出て、エラーメッセージはポップアップされます。
今の例は、SMLの小さなプログラム断片に対する継続的チェッキング（continuous checking）でしたが、Isabelle/jEditでは、大規模な証明ドキュメントに対しても、全体の整合性を常に監視し続けます*2。これは重い処理になり得るので、チェックの要求と応答は非同期的にやり取りされます。また、マルチコアCPUのネイティブスレッドを活用した並行処理によりチェックの高速化を図っています。
ウェンツェルのPIDE構想
Isabelleプロジェクトはロレンス・ポールソン（Lawrence Paulson）によって創始されましたが、現在、プロジェクトを牽引している中心人物はマカーリオス・ウェンツェル（Makarius Wenzel）です。
ウェンツェルは、証明支援系のユーザーインターフェースの革新を推し進めています。宣言的な証明ドキュメントに対する良好な編集GUIと、非同期／並列／継続的なチェッカーを緊密に連携させようとしているのです。その方式はPIDE（Prover IDE）と呼ばれています。PIDEの発音は次のようらしいですね。
PIDEはソフトウェア・アーキテクチャ／フレームワークの名ですが、形がそれほどハッキリしているわけではなく、ウェンツェルの思想／構想だと言ったほうが適切でしょう。
この構想を実現するために、証明支援系ユーザーインターフェースの“大将”であるProofGeneral/Emacsと袂〈たもと〉を分かち、一番メジャーなSML処理系であるStandard ML of New Jerseyとも縁を切っています。
NEWS of Isabelle2015:
* Support for Proof General and Isar TTY loop has been discontinued.
http://sketis.net/2016/isabelle-no-longer-supports-smlnj :
17-Feb-2016 marks the historic day when support for SML/NJ was removed from the Isabelle code base, ...
ProofGeneralの方式は、PIDE構想とは根本的に相容れないし、Standard ML of New JerseyはPIDEのための性能要求を満たせない、ということらしいです。
PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。
