進化なのか、退行なのか？

どうかしてるぜ！

Isabelleマニュアルの分かりにくさも尋常ではないが、それを執拗に詮索している僕も常軌を逸しているかもな。どうかしてるぜ。

Isabelleコミュニティの人は、「どうかしているぜ」な用語の曖昧さ／乱用を自覚してるのだろうか？ あまり意識してないような気がする。意識してれば対策するだろうが、そんな気はないのではないか。「なんでコンナことになってしまったのか？」は、部外者としても興味は湧く。

歴史的背景 - 檜山正幸のキマイラ飼育記 メモ編 :

歴史を調べないと分からない処理系、てのも困ったもんだが、

曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編 :

上記のことは、1980年代、90年代の資料を読んで分かった。いつでも、そのような由来まで分かるわけではない。「なんかの事情で、変な呼び名や言い方が発生し、それがコミュニティに定着した」という程度の予想しかできないだろうが、まーそれでもいい。

1990年のポールソン・マニュアルは分かりやすかったが、1994年の次のチュートリアルも分かりやすい。

• Title: A Gentle Introduction to Isabelle
• Author: Sara Kalvala
• URL: http://www.informatik.uni-bremen.de/~cxl/lehre/isakurs/tutorial.ps
• Pages: 12

1990年前後の論説が分かりやすいのは：

1. 規模も複雑性も今より小さい。
2. 素朴な作りで内部構造が丸見えだった。
3. 説明も、内部構造やメカニズムから始めている。
4. TTY入出力の引用が多く、これが具体例として大変に効果的。

素朴な内部構造がTTYから見えていた、わけだ。

現代では：

1. 大規模複雑なシステムに育った。
2. 低水準の内部構造を出来るだけ隠そうとしている。
3. 説明は、高水準の抽象モデルで済まそうとしている。
4. 例が少ない。

例がロクにないのがホントにキビシイ。例がなくなったのは、例の引用が困難だからだろう。

1. 例を載せるには大量の画面キャプチャが必要。
2. テキストコードの引用では、擬似コードと実際のコードの区別が困難
3. 高水準の構造化コードでは“動作”をイメージしにくい。
4. ブログ記事などでもテキストとして貼り付けることは困難（今の僕の状況）

ドキュメントに例を載せられない、のはIsabelleに限らない。

1. Coqの証明スクリプト（タクティク列）は載せても分からない。
2. Coqの証明オブジェクトはなおさら意味不明。
3. Globularに至っては、ソースコードという概念が一切ないから、どうにもならない。
4. 画面キャプチャの連鎖による紙芝居か、動画による説明しかないだろう。
5. 動画だと、英語が（僕は）聞き取れない。

絵算ベースの証明支援系 Globular - 檜山正幸のキマイラ飼育記 :

Globularは、我々のコミュニケーション形態に対する試練のように思えます。

証明支援系全般で、「使用法の伝達が困難である」という問題があり、この問題は、TTY→GUI→Pictureと発展するに従い、どんどん悪化、深刻化している。