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

NHK に主に期待したいのは自由ソフトウェアを広めることよりかはソフトウェアがユーザーを不当に支配することの問題の方かな。NHKなら行ける気がしてる。

いまは朝が辛すぎるという個人的な課題の解決が最優先だな。。。

民放はマイクロソフトとか Apple の CM 流してるし自由ソフトウェアについて報道するのは厳しそう。

NHK にはソフトウェア企業のスポンサーが付いていないのでプロプライエタリなソフトウェアの不道徳さについて報道するための潜在的な能力があるといえそう。

@manzyun 自由ソフトウェアを使ってもらいたいという感じではなくて、ソフトウェアがユーザーを支配している構造が存在している実態と、自由ソフトウェアという概念が存在することを報じて欲しいという感じですね。

NHK に DRM の邪悪さをどうにか知ってもらってまずは NHK プラスから DRM が消えるようにしたい。。。

自由ソフトウェアを広めるために NHK に働きかけるのは日本ではかなり合理的な戦略な気がする。

NHK で自由ソフトウェアの特集が組まれるようにならないかな。そうすれば自由ソフトウェアの認知度が爆上がりしそう。

NHK にしかない魅力的な番組が存在しているのだとすれば、それは資本主義社会の限界を証明しているのかもしれない。

NHK が資本主義の枠組みから離れて存在していることは結構重要なことだと思ってる。

資本主義社会だし自然にそうなるよなーと最近は思うようになった。

パラリンピックはあんまり好きではないけど、ほぼ全局で昼間じゅうオリンピックの中継やってたのにパラリンピックは一切中継をやらない民法って"視聴率至上主義"で一貫しててある意味すごいよね

ACL2 でバブルソートするやつ停止性を証明するのにどういうメジャーを定義すればいいかは考え付けたんだけど、実際に ACL2 で証明するの大変そうだったのでやめた。私にはまだ配列は早かった。もう少し List を使ってやっていきたい。

いま SICP 会をやっているんだけど、普段 ACL2 を使っているせいで無意識に defun と書いてしまう。

普段体調悪いと感じたとき大抵は 36.2℃くらいなんだけど今は36.7℃なので発熱しているのかもしれない。

昨日 ACL2 でバブルソート実装しようと思ったんだけど停止性の証明だけでも大変そう。戦略は思いついてはいるけどまだ実装できてない。

ACL2 の Arrays は論理的にはただの連想リストなんだけど、特殊な形をした連想リストを制約を守って使うことで実際には配列として処理するものみたい。定理を記述するときは線形時間かかるけど副作用のない扱いやすい連想リストとして使えるが、実際にプログラムを走らせる時には配列として扱われて速いって感じ。

Guix じゃない仕事の環境では Emacs のパッケージ管理をほとんどしてないな…。適当に package-install してる……。

Guix とともに生きていくとので Emacs のパッケージ管理は Guix でやってる。

Stobj を学んで、これで ACL2 での副作用も楽勝だぜって思ってたらなんか Arrays っていうページもあって困惑している。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____ARRAYS