Timeline for it list by senooken, page 50

ACL2 は定理をただ書けばいいわけではなくて定理を書くことで ACL2 をプログラミングする感じなので初見だと意味が分からないんだよな。たとえば、 `(equal x y)` みたいな定理があったとき `(equal y x)` は式としては同じだけど ACL2 の rewrite ルールとしては全然意味が違う(ACL2 は equal の左にあるやつを右に置き換える)とかいうのを知った瞬間にこれは厳しいってなる人はたくさんいるんじゃないだろか……。

でもその壁を乗り越えるとちょっと関数が複雑になっても定理証明できたりして結構楽しいんだよな。こんな感じでなんか ACL2 で楽しんでいる層を増やして ACL2 界隈を日本に構築したい気持ちがある。

「ACL2 証明」で検索するとマジで私の記事が上の方にでてくるのつらいな。どんだけ人気ないんだ ACL2……。

なんか楽しいし ACL2 で定理を証明してみて公開していっているんだけど、私にはそれだけ読んで ACL2 を実際に少しでも使えるようになるための学習ができるほどの情報を提供できるスキルがいまのところないんだよな。

全ての記事に公式チュートリアル読め(本格的なチュートリアルには10~40時間かかるって書いてある)って書いたらそれはそれで ACL2 のモチベ下がりそう。ただ希少情報提供者の責務として全ての記事に公式チュートリアル読めは書いた方がいいかもしれん。

ACL2 は Lisp と定理証明にめっちゃ興味があるという極稀なケースか何故か ACL2 を使っている研究者や、仕事で実用しているわずかの会社でしか使用されていないわけでなんかライト層を増やすのは無理ゲー感がある。

なんかどうしようもない気持ちになってる。

modulo 関連のライブラリ、これ強そうだな。これを使えばこの前挫折したリストの回転の記事でリストを一回転したら元に戻る証明いけるかもしれん。

https://github.com/acl2/acl2/blob/9e1ad7d075c1f825d9afae2ef63eb6dda3655f3a/books/kestrel/arithmetic-light/mod.lisp

以前は password-store 使ってたけど今は Nextcloud Password 使ってるな。Nextcloud Password は Nextcloud の運用を始めないと使えないのがネック。

Korpiklaani っていうバンド知った。森っぽい感じでよい。

この人が新しい GLORYHAMMER のボーカルっぽい。これは謎の王子感があっていいな。バンドメンバー確定しててよかった。

Gloryhammer on Instagram: “Mighty warriors of the galaxy! From the distant enchanted realm of Cyprus, a new hero has risen to wield the Astral Hammer and make epic…”https://www.instagram.com/p/CW6iK2EKv0j/

Legendary Enchanted Jetpack - YouTubehttps://www.youtube.com/watch?v=Rqe0VbRQ4Wc

新しく GLORYHAMMER の持ち主を探す必要が生じているのか。

え、GLORYHAMMER で GLORYHAMMER を持つ人もういないってこと？

GLORYHAMMER から2021年8月に主人公っぽいアンガス・マクファイフ13世が脱退してることに気づいてしまった。これはショック。

記録みると結構ハフマン木の記事を書いてるんだけど、ちょっとこれをまとめて一つの記事にするの大変すぎるのでなんか別のことやって別の記事作ろう。あまりに大変すぎる。

昔書いたハフマン木のコード、弱いルールを書いているな……。苦戦したのはこれのせいでは……。

それぞれの言語でちゃんと本気でチューニングしたのか問題が生じそうなやつだ。

Scheme の謎の iota を思い出してた。ここの回答と同じく素数夜曲で index の i をより印象的にするために iota にしたみたいなことを読んだ記憶あるんだろうけど本当にそうなのかな。https://ja.stackoverflow.com/questions/41427/golang-%E3%81%AB%E3%81%8A%E3%81%91%E3%82%8B-iota-%E3%81%AE%E5%90%8D%E5%89%8D%E3%81%AE%E6%84%8F%E5%91%B3%E3%81%AF

まず iptables 使ってるところがあったら v6 用の設定も書かないといけないとかあるし、それだけみただけでもちょっとつらすぎなんだよな。

まあゲーム業界はもう IPv4 だと限界きたみたいだし、IPv6 と両立させる知見についてじゃんじゃん公開していって欲しいところ(他人任せ)。

しかし IPv4 アドレス枯渇の危機が訪ずれても(実はもう訪ずれている) Mastodon は崩壊しないことが分かってちょっと安心だな。

個人的な問題は私のメールサーバーで対応するのちょっとだけ大変そうなんだよな。

既存のインフラについて IPv4 を維持しつつ IPv6 を両立させてメンテするのはつらすぎるんだよなーーー。

いやー今やっているやつよりも IPv6 に対応することの方が重要ですよとか進言するための根拠が薄すぎる。

IPv6 のモチベあるのゲーム業界くらいでしょってところがある。

IPv6とゲームの課題に向き合ったJAIPAのゲーム・エンタメWGの活動とは？ (1/4)https://ascii.jp/elem/000/004/084/4084962/

正直、利潤追求しないといけない企業にからすると IPv6 の対応を後回しにしたくなるのはめっちゃ分かる。いろいろ頑張って現状は IPv4 で回ってるし。