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
きゅーけー@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
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 11:23:50)
TypeScriptはas, !, is, anyをすべて避けたうえで安全性を高めるすべての tsconfig を書いた上であらゆるリンターを有効にした上で危険
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:58:26)
TypeScriptに対していままで過度な期待をしていたことがよくわかったのでそれは本当によかった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:48:52)
12月中に定理証明の記事を投稿することを目指して執筆しているというのに、貴重な時間をしょうもな矛盾の存在証明に使ってしまった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:22:50)
TypeScript、一見安全そうにみえる7行のコードで任意の型(neverを除く)になりすませるというこの現実。
```
const convert = <T, S>(value: T, witness: S): S => {
const obj1 = { a: witness } satisfies { a: S };
const obj2 = { a: value } satisfies { a: T };
const empty = (): {} => obj2;
const obj = { ...obj1, ...empty() } satisfies { a: S };
return obj.a;
};
```
https://qiita.com/tojoqk/items/1e37896757f847c97948
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:01:56)
今日TypeScriptに感じた激しい怒りを怒りのままにするのではなくて、冷静な記事にして公開したとで収まった感じがする。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-12 23:42:52)
QIitaにTypeScriptの記事を投稿しました。
TypeScriptはあんまり自分のサイトにはなんとなく書きたくないからQiitaに書いた。
https://qiita.com/tojoqk/items/1e37896757f847c97948
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-05 01:07:04)
これでロック解除が超快適じゃん。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-05 01:06:44)
Fedoraでいまふと思って指紋のやつ使えるかなあって思って試したらできた！えー、指紋認証できるのか、これは超びっくり！
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:57:40)
ACL2がいろんなヒューリスティックを駆使して自動で定理証明するのはまさに実用Common Lispに書いてあるヒューリスティックな探索の話に通じるように思う。
Older Notes