Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:51:37)
等式に方向があるのはACL2のメリットだと前から思ってはいたんだよなあ
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 22:44:21)
食洗機で圧力鍋洗えるの革命すぎる
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:26:53)
ACL2で証明した定理をそのまま移植するなら普通のAgdaじゃなくてCubical Agdaのほうが良さそう
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:21:28)
ACL2は、ぷよぷよの連鎖がどこで止まったか教えてくれて連鎖を始める前に戻して何度でも盤面を調整してやり直せるイメージ
諏訪子@suwako@sns.076.moe (2026-01-06 22:17:48)
一部ウェブ・ソフト開発時代のソースコードを再公開した（C言語＝５個、Go言語＝１個）
https://github.com/TechnicalSuwako?tab=repositories
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:12:33)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:39:37)
これは完全にトレードオフだな。危険だけど大連鎖の爽快感を楽しみたいなら ACL2 のほうがいいけど、緻密にかつ安全に進みたいなら Cubical Agda のほうが良いという感じ。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 21:32:13)
良識
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:27:36)
ACL2の記事書くならCubical Agdaをやってからのほうが良さそうだな。まだ理解に自信はないけど、おそらくACL2はぷよぷよで大連鎖を起こすようなスタイルで、Cubical Agdaは電車の線路を引くような感じで明示的に安全性が保証された連鎖を記述する感じなんだと思う。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:01:11)
ACL2をヒューリスティックから型理論に昇華したもののような気がしてきた。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:57:09)
Cubical Agda、もしかしてACL2で身につけた感覚がとても役に立つものなのでは…？
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 20:38:07)
体調が悪すぎる
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:27:22)
guixとnixの両方が入ったFedoraになってしまうな。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:26:54)
1labのためにnixのインストールが必要らしく流石にこれは自宅で実行したほうがよさそうな感じだな。。。
ずいぞう☕🦜:skeb_logo:@zuizo@misskey.design (2026-01-06 20:09:47)
近くにおいしい食べ物屋もたくさんあることだし
#ごぞんじゲーム部 #一次創作 #漫画
---Attachments---
https://file.misskey.design/post/ef214efe-78e9-4055-a232-8c2abc79b843.webp
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:08:37)
1labのドキュメントを読んでいくのが良さそうな雰囲気らしい
https://1lab.dev/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 19:40:39)
これからはCubical Agdaの学習に集中したいと思う。学習する価値が極めて高い気がする。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 19:16:09)
OSC大阪について考えている
Rikuoh Tsujitani@riq0h@letter.mystech.ink (2026-01-06 18:08:53)
疲れすぎてしもつかれになった。
Reply to @tak4
たかし@tak4 (2026-01-06 17:44:49)
bibisもサブディレクトリに入れれば良かった。
その場合、bibi.i2p/forum/ みたいなurlになる。
Reply to @tak4
たかし@tak4 (2026-01-06 17:36:29)
ホストは物理的に一台、デーモンもopenbsdのhttpdが動いてゐるだけ。
bibiはウチのhttpdの愛称といふことにすればいい。
たかし@tak4 (2026-01-06 17:30:16)
サイトのurlはホスト名をbibiにして bibi. なんとか . tld にすればよかった。
変更する予定はないけど、moeドメインを手放す事情ができたら、さうする。
Shorty(デジタルかめランド)@shorty@fedibird.com (2026-01-06 17:13:50)
静的ページ、ローカルPCでサクサク編集できるの気楽でいいよね。本番環境いじるまで無限にシミュレーションできる
おもちゃの感覚で自サイトいじってる
Reply to @tak4
たかし@tak4 (2026-01-06 16:50:00)
トラッキングURLブロック機能はオフにした方が楽。
あとデフォルトで広告ブロック用のhosts.txtを読み込むのは人によっては嫌かも。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 15:36:23)
なにかしててもしんどいし何もしてなくてもしんどい
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)
数学基礎論と物理学を組み合わせる研究はすでに進んでいて、小澤正直教授によって劇的に進展していたということを知った。数学基礎論って物理学にも応用されてたのか。。。
Coro@Coro@mstdn.maud.io boosted:
@hswugbhxwsz@best-friends.chat (2026-01-06 12:44:21)
【悲報】母親のスマホ、マカフィーとノートンを携帯ショップで同時契約していた事が発覚
なおAdblockerも契約していたがこれら全てインストールされていただけで有効化されていない模様
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 13:48:20)
昔BitZeny掘ってたっけなあ…懐かしい
Ubuntu@hswugbhxwsz@best-friends.chat (2026-01-06 12:44:21)
【悲報】母親のスマホ、マカフィーとノートンを携帯ショップで同時契約していた事が発覚
なおAdblockerも契約していたがこれら全てインストールされていただけで有効化されていない模様
Older Notes