[Agda] Agda Lectures at CVS

産業技術総合研究所の研修コース「 Agda による仕様記述」に参加しました。

以下は私の参加した10月の回の話。もしかしたら11月は10月の参加者の反応を見て内容が変更されるかもしれません。

一言で言うと
Coq, Agda のような定理証明系とか依存型の関数型言語とかに興味のある人が、概要を知るには良い二日半のコース。参加費無料なのもポイントが高い。お薦め。（開催が大阪なんで関西周辺以外の人にはちょっと厳しいが）

もう少し詳しく説明すると
「Agdaの持つ依存型の機能を使って、仕様の制約を型として表現すれば、機械的に検証出来るよね」というところに主眼を置いているみたいです。なので、定理証明の部分は従であり、主眼は仕様を書ける様になろう、ということのようです。
とはいえ、仕様の制約をAgdaで書く以上、書いた関数が仕様を満たしていることを示す必要がある訳ですが...。

が、まぁ当たり前と言えば当たり前なんですが、二日半ではAgdaを使いこなせるようにはならなかった...。まぁJavaだってHaskellだって二日半では使える様にはならない訳で、当然というか仕方が無い。なので、「Agdaがどんなものなのかの概説を聞く」ぐらいに考えていたほうが良いです。
とはいえ、Agdaに関する日本語の資料はほとんど無い現状で、テキストの説明を聞き、判らないところを教わりつつのハンズオン実習がある訳で、価値は大きい。

参加者は結局８名。堅苦しさの無い普通のIT系勉強会のようなフレンドリーな雰囲気で、質問しまくりみたいな。逆に言うと講義内容がまだきっちりと固まっている訳では無い感じです。
にわとり小屋でのプログラミング日記のCoqな今井さんとお近づきになれたのも良かったです。数人で２日目の夜に懇親会したのですが、最初からちゃんと計画して全員（講師の方にも声をかけて）でやれば良かったと反省。
＃話に出た紫色の本は、"Handbook of Practical Logic and Automated Reasoning" (John Harrison, Cambridge Univ. Press, 2009) です＞今井さん。

とにかく私は楽しかったです。代休消化で関西旅行した価値がありました。参加させて頂き、ありがとうございました＞CVSの方々。

参加の前提について
募集要項には「プログラムを書いた経験(言語不問)、またはシステムやソフトウェアの設計に従事したことがあること。」「Emacs で文書を作成編集した経験があること。」と書いてあるんですが...。
うーむ、HaskellとかOCamlとかの類の型付き関数型言語の初歩的な知識があったほうがいいかも。モナドとか別に知らなくてもいいけど、簡単な再帰とかパターンマッチとか使って List の map とか length とかぐらい書けたほうが良いかもしれないです。そうでないと初日の演習問題でいきなり困るかも。あとはまぁ、ペアノの自然数( 3 = succ(succ(succ(zero))) みたいな話 ) も知ってた方が良いかなぁ。
ただ、参加者の関数型言語への習熟度を見て調整していたかも知れないので、11月はどうなるかは判らないです。