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

stobj を学んで ACL2 で色々できそうな気持ちになったけど何も思いつかない。

今の体調不良は実は過去に無自覚に無症状で感染していたコロナの後遺症なのではないかと思うことがある。

今体調が凄く微妙で出勤するかどうかかなり悩んでる

まったく眠れない

stobj を学べただけだけでおおきな進捗といって良さそう。

破壊的変更をするだけじゃなくて操作の性質の証明までできるからな。論理的には副作用はなく書けるから強すぎる。

ACL2で破壊的変更をする関数を書けるようになって最強になれそう。まずはライフゲームとか作ろうかな。

これだけみると更新するのに過去の値とはって感じだな。stobj は副作用のない世界で不可逆な変更をするための仕組みって感じで、副作用のある関数を導入することなく実際には破壊的な変更をするための仕組みって感じ。副作用のない世界では更新する前の変数とかにアクセスすれば、過去の値を見れるわけだけど見ないことを証明できれば破壊していても破壊していなくても差はないってことだな。

ACL2 の stobj を勉強してる。なんかこれで ACL2 で副作用を扱えるっぽい。構文的に更新前の過去の値が参照されないことを証明することで破壊的変更を OK とするみたい。面白い。

企業特有のクソ利用規約(一般ユーザを訴える条件を羅列する感じのやつ)じゃないだけでも最高だな。

XP-PENMac_3.2.0_210814(New UI Driver) っていうドライバのライセンスが LGPLv3 だった。https://www.xp-pen.jp/download-330.html

XP-Pen って会社の左手デバイスが macOS でうまく動かないという相談を受けて確認したところ、macOS のアクセシビリティへのアクセスを許可していないのが原因だった。

また、XP-Pen の左手デバイスのドライバのライセンスが LGPLv3 だったので感動した。自由ソフトウェアとしてドライバを公開している企業が存在するとは驚きだ。私の XP-Pen 社への評価が爆上りしてる。

Guix でスクリプトを書くなら ACL2 よりも Guile の方が合理的なんだよなー。

UptimeRobot の有料ユーザーなので、ハートビート監視でなんか色々監視する対応しようかな。

最近は ACL2 で友人の書いたプログラムのアルゴリズムを証明してるんだけど、そうじゃなくて自分でなんかやりたい気持ち。

なんか ACL2 でスクリプト書きたいけど何も思いつかない問題が発生してる。

反出生主義、そもそも生まれることについて思い通りにならないという問題があると思う。仮に地球上で何も生まれなくなっても生まれることのどうしようもなさは何も解決しないんじゃないかな。宇宙広いし。

行動分析学を生かした小学校ができるみたい。革命なのでは。

https://twitter.com/nishikarugakuen/status/1428506488906027011?s=21

どこまで program モードの範囲を限定できるかが肝だ。

ACL2、program モードで関数を定義すれば何も証明してくれない代わりに副作用使い放題なことがわかった。これで ACL2 でスクリプトをバリバリ書いていけるぞ。