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

デジタル庁のサイトを GNU IceCat のデフォルト設定で開いたときの画面

GNU IceCat でもまあまあ色々できる。普通にブラウジングするだけなら GNU IceCat だけでよい。なんか予約とか購入とか重要そうなやつだけ Firefox 使おう。

デジタル庁のサイトが GNU IceCat のデフォルト設定で閲覧できないという面白体験をしてしまったので、GNU IceCat ユーザーに戻りかけている。

浄土真宗の現世利益についても自由意志信念を捨てることによる益と解釈できる。浄土真宗で信心を獲得すると行動の主体が「私」から「南無阿弥陀仏」に置き換わる。これは自身の自由意志信念を捨てることであり、現世利益はこれに付随して得られるものだとすればなんら不思議なことでもない。

観測事実と矛盾する可能性のない宗教としては浄土真宗がおすすめ。浄土真宗の教義のメインは死後の不安の払拭であり死後について観測不能である以上は観測事実と矛盾することはない。

気象予測の技術が発展したことで雷様の存在を信じるものは少なくなったと思う。自由意志に対しても同じことが起こるか。

ヒトの行動の予測と制御の精度が上がったとき、自由意志の存在が観測事実と矛盾することになって自由意志も宗教的な信仰の対象とみなされる未来が訪れるのだろうか。

この銀河を統括する情報統合思念体になりたい……

何かしないと鈍りそうなのでなんか ACL2 で定理証明する。

え、じゃあ何食べるのって思ったけどそういう話ではなかった。

今日は一切定理証明は進んでないけど、人に勧める ACL2 の実行環境は ProofPad と分かっただけで大きな進捗だ。

ACL2 の証明の過程がグラフィカルに良い感じに表示されたりするなら、乗り換えも検討したけど残念ながらそういう感じではなさげ。

ACL2 professional は Emacs を使ってるらしいのでもう、Emacs から乗り換える必要性はないかな。

ProofPad がちゃんと考えられて作られていたことがよく分かるな。ACL2 の入門する人には ProofPad をおすすめしよう。自分は Emacs を使うけど。。。

https://arxiv.org/pdf/1304.7856.pdf

最新の proofpad は Web で Websocket で ACL2 と通信する感じなのか。。。これユーザー増えたら破綻するんじゃないだろうか。大丈夫かな。http://new.proofpad.org/

今私が使ってるのは古い proofpad なのか。https://github.com/calebegg/proof-pad-classic

ACL2 の IDE である ProofPad をインストールしたんだけどこれ良さそう。Emacs で開発しているときよりもちょっと体験が良い気がする。。。Paredit が使えないからエディタとしては微妙なんだけどリアルタイムに証明してくれたり、あんまり見なくてもいい情報を目にしなくて済んだりするからな。

GNU Guix で ACL2 Sedan のために Eclipse をインストールしたいので icedtea なるものをインストールしてる。

そもそもソフトウェアによって行動がコントロールされていると自覚している人ってあんまいないのかな。

NHKってよくすぐには到底解決できないような問題もドキュメンタリー番組として取り上げたりしてるしそんな感じでプロプライエタリソフトウェアの不道徳さだって報道できるでしょ。