Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 58

しばらくは ACL2 やろう。定理証明面白い。

とりあえずここら辺の問題を解き直すか。忘れてるし。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____INTRODUCTORY-CHALLENGE-PROBLEM-1

ACL2 は簡単過ぎる問題をやってもなんか訓練にならないし、難しすぎる問題をやると詰むのでほどほどのやつがいいんだけどほどほどの問題が何なのか最初は分からん問題がある。

何やっているときに、ACL2 が消去されたのか思い出せんな。

L-99 の P23、乱数必要じゃん。これは死んだ。

まだ最初の 21 問しか解いてないのでいつから難しくなるのか分からん。

LISP-99 にでてくる最初の方の関数はとりあえず簡単な関数でそれに関連する定理も割と簡単に証明できるんだよな。

ACL2 は簡単な関数の簡単な定理を証明している限りは楽しいんだよな。難しいやつは消去バーストが長く続かないと無理。

なんか色々考えた結果、ACL2 を再びやろうという謎の結論に至った(極端)

今日、めっちゃ寒いし雨も冷たくてつらかった。

自力で Typed Racket みたいなのを作るの大変すぎると思うんだよな。めっちゃマクロ書かないとじゃん。

本当は Racket じゃなくて Guile を使いたい気持ちがあるけど Typed Racket があるから Racket を使ってる感があるのがよくない気がしてる。

(cdr nil) は百歩譲っていいとして (car nil) が nil なのはおかしいじゃん。

Common Lisp だと nil は List なので describe をみても nil の可能性に気づけないし (car nil) の値も nil だからやばいじゃん。

Scheme の cond の => はめっちゃ好き。しかしこれが生きるのはその関数が偽を返すかもしれないと認知しているときなわけで……。

やはり静的型は要る気がしてきた。string->number という名前にもしかしたら #f を返すかもよ要素がないのがよくない。

Schemer で string->number の結果が #f かどうかを調べるのを忘れたことのない人が果たしているのだろうか？

やはり型はいるのか。Common Lisp なら check-type をちゃんと書くようにすればちょっと安全になる気がしてる。

その 99.9% の問題であるどこかで生まれた謎の nil が最大かつ深刻な問題なんだよな。

Typed Racket は絶対に空じゃないリストとか、負でない整数とかを型で表現できて「あー、それくらいの表現力は欲しかったわー」っていう程度の強さがあるからかなり良い。

ここまでのほどほどな強さがあればなんか欲しい気持ちになる。