Show newer

ACL2 で証明をすると最終的に答えに行きつくまでの道筋を失なってしまうので、マインドマップに試行したことをメモしながら証明しようと思う。

undefined じゃなくてもっと激しく爆散して欲しい

Show thread

JavaScript、なんか都合の悪いことが起きるとすぐに undefined っていうのやめて欲しい。

最近、なんかよく分からん仕事をやる人になってて厳しいな。SREとはって感じになってる。なぜ私は JavaScript を書いているの?

300 円寄付してくれっていう圧がすごい。あとでするか…。

Show thread

Wikipedia から唐突に「あなたは特別な存在です」とかいうメールが来てなにかの勧誘かと思った(再寄付のお願いメールだった)。

生活環境の変化によって、スマホで ACL2 ができることがもとめられるようになった

大変だったアピールするためには解説記事書くしかないな

Show thread

やっぱ、ACL2 は自動証明なので後からコードだけ読んでもそれがどうしたって感じになるなー。

Show thread

これを証明するのすごく大変だったんだけど後から見返すと全然大変じゃなさそうなの困る。

Show thread

早起きしたけど仕事は9時からでいいかな

そんなに伸びてるわけではなくてもかなりまともになった。

Show thread

ショートスリーパーかもしれない気がしてきた。早く寝ても睡眠時間はそんなに伸びない。

A ならば B が真の時に B ならば A と思っちゃう現象、刺激等価性の話と関係があるかもしれないんだよな。ヒトよりも他の哺乳類や鳥類の方が論理的に学習をしてると言えるのかもしれない。

「AならばB」の場合に「BならばA」とは限らない。

これは、

初音ミクはボカロですが、ボカロだからといって初音ミクとは限りませんよね?

ってだけの話なので、やはり例がわかりやすければ子供でも理解出来ると思う。

まだ「不自由なソフトウェアをみんなでボイコットしよう!」ということができる段階になってない。本当の意味で自由ソフトウェアについて知ってる人があまりに少なすぎる。ITエンジニアとそうでない人の集団を比較してもほとんど差がないといって良いレベルで知られていない。

完全に自由ソフトウェアのみを使って生活することができない人でも、自由ソフトウェアを広める運動をする資格はあるということも訴えていきたい。自由ソフトウェアのみを使って生活できない現状に問題があるのであって、自由ソフトウェアを使って生活できない人が悪いということではない。

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!