Conversation

私は静的型付き言語も好きなんだけど、私は絶対に失敗しないと分かっているのに Maybe 型とかを使いたくなってしまうような状況がもの凄く嫌で、そういう状況が限りなく少なくなるようなプログラミング言語を求めてしまう。Typed Racket は正の整数型とかがあるので、普通の静的型付けのプログラミング言語よりはちょっと強いけど全然足りない。

そういう理由があって私は ACL2 のような定理証明支援系に手を出しているわけだ。