Agda のせいで眠い

まぁ、ゆっっくりやってますが、なんとなくわかってきた。いや、まだ自在に使えるってわけではないですが。

なんだけど、つい朝の四時まで Agda に触りまくってしまって、なんとなく八時には起きちゃったし。なので、とっても眠いです。昔は、そんなの全然平気だったが、さすがにこの歳だとな。つうか、また、咳と鼻水がぶり返したりしたら嫌だ。

この手の証明系は複雑なくせにできることがしょぼいので、学生たちには退屈だろうなぁ。普通のプログラミング言語での記述の4乗ぐらいかかる説がある。一方で、証明できるのは一面だけで、全体がバグがないことは保証されないし。とは言え、必要なところには使わざるを得ないからなぁ。

この手の証明ベースの構成的手法はダメだっていう人も多いみたい。特にモデル検証系の人達ね。まぁ、五十歩百歩だろって気もします。人間がプログラミングしているうちはダメだよねとも思う。何を作って欲しいかも、ちゃんと伝えられなかったり、正しく動いているかどうかも判断出来なかったり。

今年は証明系に興味がある感じだけど、それも一つの方向ってだけですね。