Coqチュートリアル#1 行ってきた

気になっていたところに Formal Methods Forum主催Coqチュートリアル＃1があったので、どんなもんかと聞いてきました。
当日の資料もリンク先に挙がってますね。

受講者は8人くらい？来てました。
Formal Methods Forumの @tmiya_ さんが主に解説して @kencoba さんがフォローという形。

tutorial.vをCoqIDEで眺めながら、普通の言語と対応付くように文法を丁寧に解説してくれてるのを聞きつつ、
証明を記述する文法と流れが分かった…ような分からんような…？（え ド・モルガン則の証明をする演習までで第一回終了。
(隙を見てはvimでどうにかならないかググリつつやってましたけど、その場ではどうにもならず。どうにかしたい。)

二時間で且つ手取り足取りな感じなので、こんなモンでしょうか。
講師の@tmiya_さんがガリグ先生の資料推しだったのでチュートリアルと平行して読めればいいなーという感じ。

次回は2月のアタマにやるみたいです。
人数増やしていきたいらしいのでCoqが気になる人は行きましょう！