06:30:01 # Life なんかCoqちょっといじっててよくわからないなぁとおもってググった。 証明とプログラムってどういう関係があるんだよというのがいまいち直感的じゃなかったんだけど。 Curry Howard Isomorphismを眺めていてなんか腑に落ちた。 あとなんかこのブログ、昔読んでた記憶が蘇ってきた。 具体的には、Coq触ろうとして挫折するたびに読んでる。