Home | Notifications | New Note | Local | Federated | Search | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo
Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバー(Docker on Guix System)を運用しており、このアカウントはそのサーバーで唯一アクティブなアカウントです。
Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Typed Racket での趣味開発がメインです。
個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
259 notes, 1 following, 1 followers
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-30 01:56:27)
Guix、「ビルド再現性」をお題目にした以上プロプライエタリなソフトウェアは一つ残らず排除しなければならないというところによって、自由ソフトウェア主義者以外にも自由ソフトウェアの価値を分からせることができるという強い力がある。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 23:11:45)
たぶん、消したときの意思決定としては301リダイレクトを数年したからもういいだろうという判断だったのだと思うけど、自分が古いURLで記事をリンクしていたことを忘れていたらしい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 23:10:23)
RE: https://mastodon.tojo.tokyo/@tojoqk/104366447696475354
よし、約6年前の記事がリンク切れになっていてさっきまでリダイレクトされていなかった問題を解決した。
(どこかのタイミングで消してしまっていたリダイレクト処理を修正した)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 22:40:43)
まあでもどうやったら直せるのか完璧に分かったので助かった
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 22:39:37)
magit-blame、rename する前の変更履歴までなんか追跡できてるな…
古いURLから新しいURLをリダイレクトを対応は2022年の10月に入れたらしいけど、それをいつ消したのかは分からん……
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:41:27)
なるほど…、サイト自体はもんだいなくて古いURLが死んだだけか。
古いURLをリダイレクトで維持するどこかの対応で消しちゃったっぽい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:36:16)
重要な記事がリンク切れしてるじゃん……。早く直さなきゃ……
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:33:41)
いままでに19Kも投稿していたようだけど、いったい何を投稿していたのだ…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:32:52)
せっかくMastodonをGuix Systemで動かすようにしたんだから、もっと活用したいなあと思うけど、わりと長い間全SNSをあんまやってない期間があり、どう活用すればいいのかよくわからんくなってるな…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:30:06)
オプトアウト方式のサービスがいまのところ生まれてなさそうでよかった
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:26:52)
Blusky に繋げたい気持ちは今のところないので Bridgy Fed のオプトインはしなくていいか…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:08:48)
@kuropen
なるほど…、下記サイトにアクセスして理解しました。
ありがとうございます。
https://brid.gy/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 09:00:36)
なんもわからん…。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-28 08:58:50)
あれ？Blueskyと繋がってるのか…？
元のページにアクセスすると bluesky っぽいサイトに飛ぶんだけど……
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@jp.bsky.app@bsky.brid.gy (2026-04-03 09:00:04)
日本のBlueskyユーザーの皆さん、こんにちは！👋
英語以外の言語として初の、日本語公式アカウントを開設しました。
今後、 @bsky.app@bsky.brid.gy などの投稿の翻訳、日本向けの告知などを行っていく予定です。
ぜひこの投稿をリポストして、多くの方にこのアカウントを知っていただけるようご協力ください。
---Attachments---
https://stropharia.us-west.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:ry3hbexak5ytsum7aazhpkbv&cid=bafkreihis2tla5ofcii6zjk2kageob3holppz4l67dym2wmpj5xlyofn74
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@kyu3a@social.vivaldi.net (2026-05-27 19:02:52)
DuckDuckGoのユーザー数が急増、Google I/OでのAI関連の発表を受けて - GIGAZINE
https://gigazine.net/news/20260527-not-google-but-duckduckgo/
『特にアメリカのiOSユーザーで伸びが目立ち、従来型の検索体験を求める動きが広がっています』
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:29:43)
Xはログインしないとタイムラインがまともに読めなくなったあたりから見なくなった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:23:06)
世間の型の価値がどうなってもAgdaが最高に素晴らしいことになんも変化はない
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:20:37)
まあ、私はXエンジニア界隈からは離れてひっそりAgdaを書く生活を送ろう…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 21:36:47)
新しい型チェッカーとして話題になっているRubyのRigorというソフトウェア。少なくとも現状の私の理解の範囲ではあんまり聞いていていい気持ちにならない…。
テストにかかれている情報を型推論に使うということだけど、それは存在命題の証明を得ているということであり、矛盾の存在を証拠にコード上のバグを検出できるということに価値はあると思う。
でも型システムとして一般に期待することは全称命題を型システムが証明してくれていることだと思うので、「型チェッカー」と聞いて期待するものと違いすぎるように思う。仮にこのような仕組みが「Rubyの型チェッカー」として広まるようなことがあれば、型チェッカーという言葉の価値が毀損されてしまうのではないか…。
これが「セマンティックなLinter」みたいなキャッチフレーズであったら何も思わなかったかもしれない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:50:58)
この仕組みに今回 agda コードを載せる場合のロジックが追加されたと…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:49:53)
過去記事を振り返ってみたら、私の闇のお手製な静的サイトジェネレーティングについてしっかり記事を書いて公開してるじゃん……
https://www.tojo.tokyo/posts/create-website-with-emacs.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:41:22)
(間違って一回外からアクセスできないテスト環境用のURL貼ってしまったので一回投稿消した…)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:40:47)
Agdaのコード含めた記事を書いて自分のサイトに公開するためのインフラが整いました!
今後はこの仕組みで色々Agdaの記事を書いていきたいところ…
https://www.tojo.tokyo/posts/agda-on-www-tojo-tokyo.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:38:45)
Adga のコードを含む記事を書いて公開できるようになりました!
Agdaの記事を書くインフラがついに整ったのでこれから色々書いていきたい…
https://www.internal.tojo.tokyo/posts/agda-on-www-tojo-tokyo.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 23:07:24)
「みんなが使っているから安全」ということはなくて、むしろ「みんなをサポートしている方が対応が遅くなって危険」なんだなと感じている…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 22:43:14)
Ubuntuから完全脱却して CVE-2026-46333 が他人事になったのが一番でかい。Guix Systemへの移行と念のためssh鍵のローテーションも完了してる。
Guix Systemは修正版のLinuxカーネルがリリースされてかなり短い時間で、修正版が上がってきていたのに対して Ubuntu ではいまだに脆弱なままで修正されてない…
https://ubuntu.com/security/CVE-2026-46333
https://nvd.nist.gov/vuln/detail/CVE-2026-46333
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 12:17:24)
cryfs よさそうだと思ったけど、自分が暗号化したい粒度的には rclone についている encrypt 機能を使うのが丁度よさそうな感じだった。
(自分は完全なメタデータの隠蔽をそれほど求めてなかった)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 10:46:38)
調べたところ Guix のパッケージにもあったので使ってみようかな
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@LwVe9@mstdn.poyo.me (2026-05-24 10:29:35)
CryFS: Encrypt your cloud storage
https://www.cryfs.org/
昨今のクラウドストレージ検閲対策でそういうヤツない？とchatgptに調べさせたら、やっぱあるな
Older Notes