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 92 notes, 1 following, 1 followers

きゅーけー@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は結構アニメの制作やってるしな。。。

言及すると言及したことでネタバレになるから言いにくいところだけど、既に有望な作品はあるしな

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 13:38:12) 念の為確認したくなって、遊んでみたところエアーマンのところまで進んだ。一旦ここで中断しておこう。

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 12:22:41) 人生オワタの大冒険はゲームを効率的なスキナー箱に変える革命であったといえる。

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 02:27:14) 人生オワタの大冒険はちょっと触っただけで途中でやめた気がするけど、それでもまあ商用ゲームにまで大きな影響を与えたと行って過言ではない作品であるように思うわけで、流行っていた当時に触れることができたのは幸運だったなあと思う。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 02:17:25) アイワナがオワタの影響を受けて開発されたという事実があるわけで、源流をオワタとするのは別にゲームのデスペナルティを軽減してかつ難易度を上げる思想について、オワタに言及するのは適切だと思う。アイワナの方がより有名だとは思うけど。
https://getnews.jp/archives/59311

きゅーけー@tojoqk@mastodon.tojo.tokyo boosted: @nemonet@mk.nekokaze.cc (2026-01-04 02:02:14) オワタというか、メトロイドヴァニアの開発陣とアイワナの界隈が被ってたので必然的に高難易度の死にゲースタイルに変わってたってのが正しい
今メトロイド作ってるメンバーも高難易度メトロイドヴァニア作ってたスタジオのはず

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 01:44:40) ゲームのハードウェアのスペックが高くなったからこう進化したとかではないわけで、発想の転換というかゲームの考え方の進化みたいなものを強く感じる。

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 01:42:28) そもそも残機がない2D横スクロールアクションゲームという時点で当時の価値観からだいぶ逸脱しているように思う。デスペナルティはそこそこ重いのが常識だったはず。

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 01:33:41) メトロイドドレッドは探索やボスの難易度を高くするかわりに簡単にリトライできるようにする工夫がなされていて、このタイプの面白さには既視感があり、「人生オワタの大冒険」というFlashゲームの面白さを継承しているように思う。当時はものすごく異質だったと思うので、あのタイプのゲーム性が任天堂にも継承されたのかと思うととても感慨深いものがある。。。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-04 01:30:49) 年末年始に体調を崩して難しいことを考える気にならなくなったこともありずっとメトロイドシリーズを遊んでた。メトロイドプライム4 ビヨンドを遊んでメトロイドプライムシリーズが面白いことが分かったのでメトロイドプライム リマスタードも無事にクリアして、いまはメトロイド ドレッドを遊んでいるところで、メトロイド ドレッドは特にとても面白いと感じていてゲームの歴史的にもよさみを感じている。。。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-01 00:05:20) おけおめ

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-27 20:35:26) ずっと積んでいたSwitchのゼルダの伝説 夢を見る島を久しぶりに遊んでクリアした。原作は幼い頃に途中でやめてしまっていたので最後まで遊べてよかった。
Switch版の感想を検索すると発売当時のレビューが多く、処理落ちが多いという指摘が多そうなのだけど、自分は Switch 2で遊んだので全く処理落ちすることなく快適でよかった。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 14:37:04) 今年中の公開を目指してACL2の紹介記事を書いているけど一向に終わりそうにない。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 14:35:47) ACL2が継続的にメンテンナンスされていてかつ安定して使えるのはCommon Lispが安定していることの恩恵を受けてる説ありそう。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 14:34:52) 今あえてCommon Lispというのもいいのかもしれないなとぼんやり思っている。注目されていて勢いのあるプログラミング言語はエコシステムの流行り廃りも激しいから書いたコードがすぐ《腐り》始めるのが悩みどころなんだよな。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 14:13:31) 宣伝文句で分からなくても普通に口コミで流行ってくんじゃないかなぁとおもってる。「ブラウザを選択する」という考え方すら存在しない状況に選べるようなるわけで、選べる以上は話題として成立するようになるから。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 14:12:33) 下記記事のスクショによると、Braveの宣伝文句はこうなっている。

> ad block でウェブのデータ通信節約 高速アドブ…

ここは広告が表示されにくくなり、ギガの節約になるといった表現に変えないと、よくわからないとスルーされそうな気がする。
ad blockと言われて何なのかを理解できる人なら、もうBraveの存在くらい知っていそうなもので、現状の宣伝文句では、チョイススクリーンで初めてBraveを知る人に訴求できるとは思えない。

スマホ新法でアップルが外部アプリストア受け入れ準備、ブラウザーは選択制 | 日経クロステック(xTECH)
https://xtech.nikkei.com/atcl/nxt/column/18/00001/11359/

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 13:47:32) チョイススクリーンがもたらす新しいインターネットにワクワクが止まらないね

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 13:42:54) チョイススクリーンでBraveがじわじわと広がっていくのではないかと予想してる。
不適切な広告表示に困っている親御さんのコミュニティなどで爆発的に流行してもおかしくない。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-18 13:40:57) チョイススクリーンをみたかったけど、悲しいことに Android 15 にアップグレードできないらしく見れなかった。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 13:02:43) AIにさっきのコードを投げると、{} が特別な場合だから起きるんだ!普通は起きないんだ!変なことしなければTypeScriptは普通は大丈夫なんだ!とうるさいので記事のコード例を少し変えた。

```
const convert = <T, S>(value: T, witness: S): S => {
const obj1 = { a: witness, b: null } satisfies { a: S, b: null };
const obj2 = { a: value, b: null } satisfies { a: T, b: null };
const f = (x: { a: T, b: null }): { b: null } => x;
const obj = { ...obj1, ...f(obj2) } satisfies { a: S };
return obj.a;
};
```
https://qiita.com/tojoqk/items/1e37896757f847c97948
Older Notes