Home | Notifications | New Note | Local | Federated | Search | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo
Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバーを運用しています。
Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Agda 学習がメインです。
生活リズムの安定のため、深夜 02:00 から 10:00 までの間はアカウントロックをかけています。その間は何も反応しません。
個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
190 notes, 1 following, 1 followers
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:32:56)
Cubical Agdaに取り組むべきであるという根拠がまた増えてしまった感…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:13:45)
数学基礎論と物理学を組み合わせる研究はすでに進んでいて、小澤正直教授によって劇的に進展していたということを知った。数学基礎論って物理学にも応用されてたのか。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 09:30:49)
AgdaとACL2を趣味で触っていた結果、数学基礎論的な思想に間接的に触れることになり、物理学の統一理論が「存在する」ということについての非自明性に気づくように導かれた感じがある。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 08:49:06)
そもそも数学的に両立可能なのか疑問に思い始めてから、子供の頃からなんとなくあった統一理論への憧れ、超ひも理論への興味みたいなことが急速に崩れていくような感覚がある。同時に自分にはプラグマティズム的な感覚もあって、そもそも観測できない領域について論じる物理学って本当に必要なのだろうかということも考え始めるようになっていっている…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 08:26:38)
理論物理学について、マクロの世界を記述する理論とミクロの世界を記述する理論と組み合わせた統一理論を作るという話があるけど、そもそもマクロの世界とミクロの世界を同時に表現できる体系というものが存在するかどうかって自明ではないのではないかということに気づいた。同時に成立しないことが数学的に証明できる可能性すらあるのではないか…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:15:48)
ACL2は一見一回論理に限定されている分簡単そうに見えて、実際のところはバリバリ古典AIの究極成果みたいな感じで、ヒューリスティック探索のコツを掴んでいくことこそが大切だったりすることが難しい。
あと、ガードの話は書かないと静的型付け全盛期の今の時代いけない気がするものの、ガードがACL2のロジックに影響しせず、ガードはほかのガードとのみ影響し合うといったところは明らかに簡単に説明できるものではなく公式ドキュメントを読もうとなってしまうあたり大変…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:12:04)
ACL2の記事執筆、あまりにも難産すぎて苦しくなってきたので一旦置いておくことにした。。。
そもそもむずすぎるし、書いていると無限に改善点が見つかる。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 22:00:32)
もしイベントを外部のアクターに処理させたければ、まず変更と同じトランザクションで(同じデータベースに)キュー要素を積み、それをワーカーが取り出して外部用のメッセージキューに投げ直すといった方法は考えられる
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 22:06:17)
非同期処理のキューの場合結果整合性で済ますが前提なので絶対にトランザクショナルじゃないといけないわけではないが、メッセージ喪失の対策だけでも意外と大変なので最初からトランザクショナルにすればいいのに……という意図
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:07:13)
トランザクションの処理はRDBの中で完結させないとおかしくなるんだよな…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:00:18)
たしかに…、RDBでエンキューまで全て済ませるのはだいぶ正解感があるな…
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 21:56:38)
@anqou ぼくの投稿は「同じデータベース内に」と書きました
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:48:29)
まさかスマホとここまで密結合したデバイスだとは…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:47:08)
そもそもスマートウォッチの実態をよく知らずに買っちゃったところから始まってるからなあ
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:46:20)
GadgetBridgeのおかげでプライベートな生活情報をクラウド管理されることなく便利機能を享受できるようになっているので、GadgetBridgeがなかったらと思うと困る…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:42:51)
GadgetBridgeはとてもいいものではあるが、デバイスを購入した時点で、プロプライエタリなソフトウェアを前提とする販売元に利益供与しちゃう問題はあるよなあ…。Windowsの入ったノートパソコンを買ってその後にWindowsを消しているものの買ったときにWindowsに貢献してしまうとの同じ問題がある。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:31:33)
私は自分の理想が全体にとって最適な自信なんてこれっぽっちも持ってないので「自分向き」という表現をしていますが、信じる正義のある人は「良いもの」に読み替えていただければと思います
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:26:20)
ない、んだが。それはともかくとして人々はもう少し自分の行住坐臥に政治的な意味合いをも持たせうるのだということを知ってほしいとは思う。ものを買うときにはある種のものを選ばないだとか、道具を選ぶときにある種の属性に価値を見出すとか、そういう判断の一つ一つが将来の状態をより自分向きにしていくための一助となるということ。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:16:16)
私は常にプロプラなものの提供者を脅迫し続けるつもりでいるけど、そこまでの先鋭さを全員に求めは（あまり）しない
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:11:23)
これ私の方向性と割と近い。プロプラなものがあることと、そのメリットの存在を認めながらも常に代替の存在を確保し続けること自体が将来的な価値を増加させると思っている
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@anqou@mstdn.anqou.net (2026-01-05 21:26:32)
多分単純な解は無いので問題に応じてうまくやる必要があるんだと思っている
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@anqou@mstdn.anqou.net (2026-01-05 21:25:05)
これむずくて、エンキューしたあとにコミットしようとしたら DB との接続が切れて死亡する可能性があると思っている。正解を知りたい。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 20:40:52)
「非同期ジョブのエンキューはコミット後にやりましょう」というやつ、コミット直後にアプリケーションプロセスがハングして状態が宙ぶらりんになるケースを考慮してないからあんまり好きじゃない。非同期ジョブのエンキューはトランザクション中に同じデータベースに入れるべき(?)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:10:24)
まず、完全に自由なOSを使用する生活を実現するには無線機器問題の壁が大きいのでほぼ厳しいというのがある
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:08:49)
プロプライエタリなソフトウェアを使用したり娯楽として楽しんだりしつつも、少なくとも理想論として自由ソフトウェアの普及を目指す人の量を増やす必要があると思ってる
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@zetamatta@mstdn.jp (2026-01-05 21:03:30)
自由ソフトウェア運動、若干、先鋭化しすぎてしまっていて、多くの人が賛同・参加しづらいものになっているのがキツいよな
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 20:58:58)
ここ最近思ったこととしてGPLは許諾しかしてなくてなにもないデフォルトの著作権法が機能している場合と比べて、何も制限してないというのは極めて重要な事実だよなあと思う。GPLに何か問題があるとすると、著作権法に問題があることになってしまうのはとても強い。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 20:53:48)
割とよくあるテーマではある気がするけど、フィクションはフィクション、現実は現実というフィクションと現実の区別能力によって失敗しているような気がする。
そういう意味ではリアリティの追求が大切なんだろうか。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 20:51:13)
ソフトウェアのバックドアを利用して支配されてしまう系はSF系にて既によくある気がする
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 20:48:16)
久々に自由ソフトウェア運動について考えていた。究極的には政治活動であることを考慮すると、必要なのは自由ソフトウェアをテーマにした漫画やアニメを制作することなんじゃないかと思う。
実際、FSFは結構アニメの制作やってるしな。。。
言及すると言及したことでネタバレになるから言いにくいところだけど、既に有望な作品はあるしな
Older Notes