昨日聞かれたので最近やっている事について書きます。
今私たちがやってる事を一番簡単に説明するとすれば、「色んなやり方でテキストエディタを書こう」と言うふうになります。テキストエディタはプログラムの例題としてなかなか面白い性質を持っていて。
世の中には既に沢山のテキストエディタがあるし、テキストエディタの開発自体が研究の目的ではありません。新しいプログラミングの方法を実験するのに、適当な複雑さのプログラムとして取り上げたのです。様々な斬新なプログラミング研究の実用性を試してみる事が目的です。世の中にはは沢山の研究がありますが、大体研究から実用まで 30 年かかるとか言われています。研究者は夢みたいな事ばっかり言う一方で、プログラマは冒険が許されず、30 年間という時間はその溝の深さかもしれません。
過去を振り返ると、Smalltalk の画期的だったのは、新しいプログラミング手法と実用なシステムを同時に造り上げた事でした。今とは時代が違うし、なかなかそういう事は今後起こらないと思いますが、せめて私も微力ながら研究と実用の溝を埋めるために力を尽くそうと思っています。
一つのやり方として私が興味を持っているのが宣言的なプログラムです。普通プログラムというのは作業手順をコンピュータに伝える事を言いますが、そうではなくて欲しい結果の性質を伝える事でコンピュータを動かそうと言う物です。「あの醤油取って」じゃなくて、「あの醤油はここにあるべき」というのが宣言的です。
宣言的なプログラムが必要とされているのは、宣言的な方が書きやすく読みやすいからだそうです。しかし何十年も言われている割に実用化されていません。色々理由はあるのでしょうが、宣言的なプログラミングがどういう物か良くわかっていなかった事と、もう一つは言うほど書きやすくも読みやすくも無かった事だと思います。
私はこれは凄い発見だと思います。人工知能の話と似てますが、コンピュータがある前は、こういう事が難しいという事自体知られていなかったからです。まさにソクラテス的大発見です。もちろん、このような専門的な研究自は今後もどんどん発展してゆくと思いますが、それとは別に、限られた研究成果の使いどころを考えるというのも面白い話だと思います。
というわけで宣言的なプログラミングにどんなやり方があるのだろうという事を調べていて、その中で何となく二つの方向性に注目しています。一つは証明の仕組みを使う方法です。これはプログラムの仕様というのは型である。プログラムの動きを証明するには無茶苦茶強力な型と型チェックがあれば良いというアイデアです。このために Coq について勉強しています。
もう一つは単体テストの無茶苦茶凄い奴を使う方法で、プログラムの状態をしらみつぶしに調べて宣言的に書いた条件と比較する方法です。このために Alloy やブール論理について勉強しています。
どっちにしても、宣言的な表現から実行出来るコードを生成するというのはちょっと無理っぽいです。でも例えば動的言語の単体テストが型の代わりに宣言的な記述を助けるように、意外と使いどころのあるアイデアがこういう研究の中に転がってる予感がします。予感だけで全然具体的ではないですが、こんな感じです。
