『マルレク第七回テーマ:「型の理論」と証明支援システム -- COQの世界 』に行ってきました

ひさしぶりに頭がグルグルする講演(勉強会)に行ってきました。

講演の概要はここ の講演概要を読んで下さい。資料は ここ からダウンロードできます。

感想

  • 万年Haskell弱者である私には、なぜHaskellerが 型 型 型 型 いうのかが理解出来なかったのですが、今回学んだ(ちゃんと理解は出来てませんが・・・) "Propositions as Types"、 "Proofs as Terms" (PAT) から来ているのだということで、腑に落ちた気がします(まだ気がしますレベルですが)
  • Homotopy Type Theoryという最新の型の論理の証明は、なんと GitHub に Coqで書かれた証明がアップされていて検証・討議できるようになっています! プログラマーのみなさんの大好きな Pull Requestも出せます(現在0ですが、Issueはたくさん出てますね)
  • Coq は自動的に証明してくれるようなソフトではなくて、証明を手伝ってくれるソフトです。証明のやり方などは人間が指示、ようするにプログラムのような物でを書く事で、ソフトが後の単純作業をやってくれるものです。
    • また、いくつもの 演繹や定理(tactic)のデータベースを持っていて、それを検索し利用できます。
    • ちなみに通常のプログラミング言語のような使い方も出来ますが、いろいろな部分が公理からの演繹で行われるので、速度とかは実用的ではないです。1 + 10000 を計算させると Stack overflow Warningが出ます(10000 + 1 では出ません)
    • ダウンロードやチュートリアルhttp://coq.inria.fr 。日本語の入門が ここ にありました、ありがたや、ありがたや。
    • 日々の仕事に嫌気がさした時に、Coqで遊ぶと仙人の気分に浸れるかもしれません :-)