4月のふりかえり

4月は、3月28日にGo1が公開されたということで、Go言語を少し時間をかけて触ってみました。この月のはじめに「UNIXという考え方」を読んだのも影響して、gnu coreutilsのソースコードを読みながらechoやcatをGo言語で書いたりしてみました。

その過程でGo言語の標準パッケージflagがUnix的なオプション指定(具体的には -o -l -fといったオプションを-olfと書く)ができないことに気づきました。それでオプション解析パッケージを探して見つけたのが、opts-goです。残念ながらGo1公開前にopts-goは更新が止まっていてそのままでは動きませんでしたが、go fixとappendがbuiltin関数になっているという情報からすぐに修正することができました。本家の方にコメントを一応残しましたが、何の反応もないのでgithubの方にupしておきました。

ちょうどそのときLivedoor Wikiを使ってプロフィールを管理しはじめていました。blogで記事をアップするのに失敗した苦い経験から、ローカルアプリで編集するツールが必要だという考えを持っていました。Livedoor wikiの記法までチェックしてプレビュー画面を表示するようなローカルアプリはそのままでは無いようなので、Go言語で実装することにしました。

大体1日頑張って正しく書けばHTMLを出力するものができましたが、ぼくが欲しいものはパースエラーが発生した行を的確に教えてくれるものです。そして、正確にパースエラーから回復することも必要です。こうすることによって、文法の間違いが複数あっても、一度に全ての間違いを把握することができます。

このようなものが欲しいと思ったきっかけは、Go言語のパーサーがちょうどこのような仕様になっていたことからだと思います。実装もGoパーサーを参考にして実装しました。

HTMLの出力結果や、エラーの報告をテストするのには、go testではあまりにも多くのケースが必要だったので、wiki記法で書かれたファイルの中にHTML結果やErrorメッセージを書き込んで、それと実際のエラー,HTMLを比較する処理をオプション付きで実行するようにツールを書き直しました。テストは定期的に行われるようにgo testのときも、そのテストは実行するようにしました(このような処理とデータを分離したようなテストをデータ駆動テストと言うそうです)。

それからあまりにもパースを繰り返すときはpanicで離脱させるようにしたりして、できるだけ無限ループに陥るようなことの無いようにしました。しかし、どれだけテストケースを増やしても、いつも意図したように動く証明はできません。リソースがあれば、ユーザーがぼく以外にもいれば、フィードバックを得ながら、意図しない動作は極限まで減らすことができるでしょう。でも、それはもしかしたらプログラムを停止することを証明することよりも難しいことかもしれません。

ということで、プログラムを証明するとはなんだろうかと血迷ってCoqを触ってみました。自然演繹法に似たところもあって、理解不能というわけでもありません。いつかパーサーの動作に関するいつくかの定理が証明できればなと思っています。

が、どんな定理を証明すれば、ぼくが漠然と恐れていることを避けることができるのか明確でないため、証明は書くことなしにツールを公開することにしました。現在はwindows版のバイナリのみ公開しています。ツールの名前は仮にwiki2htmlと呼ぶことにしています。

しかし、ぼくが証明すべき定理を正確に把握したところで、CoqはGo言語のコードを証明できるようなものではありません。他の言語の連携はもっぱらCoqコードをHaskellやOCamlコードを生成する方のようです。ぼくがバカなのか分かりませんが、むしろ必要なのはC, C++, PHP, Python, RubyなどのコードからCoqコードを生成する方ではないかと思います。そうすれば、実際に使われているコードの証明を書くことができます。しかも証明を書く人とコードを書く人は同一人物である必要もありません。もちろんコードを書く人はCoqを知る必要もありません。