InfoQ Japanイベントレポート「Coqチュートリアル#1」

記事は速攻で仕上げました。
毎度のことですが、@tmiya_さんに感謝です。

個人的に、Coqチュートリアル実施の意味は大きい。
実施するまでは、「チュートリアル自体に目新しいことはない」
という意識があった。が、実際やってみると、
CoqIDEの細かいところから、仕様の書き方自体の話まで、
自らの考慮不足を反省する機会になった。

フォン・ノイマンが「ゲームの理論と経済行動」の1.4で、
「この理論が最初に適用されるのは、結果が自明であって、
しかも理論など実は必要としないような初歩的な事柄でなければならない」
って言ってるけど、まさにそうだと思う。

やらなくてもわかってる、ということでやらなかった場合、
結果的に何も分からないことになる。