きゅーけー@tojoqk@mastodon.tojo.tokyo: これは完全にトレードオフだな。危険だけど大連鎖の爽快感を楽しみたいなら ACL2 のほうがいいけど、緻密にかつ安全に進みたいなら Cubical Agda のほうが良いという感じ。

Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:27:36)
ACL2の記事書くならCubical Agdaをやってからのほうが良さそうだな。まだ理解に自信はないけど、おそらくACL2はぷよぷよで大連鎖を起こすようなスタイルで、Cubical Agdaは電車の線路を引くような感じで明示的に安全性が保証された連鎖を記述する感じなんだと思う。
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:39:37)
これは完全にトレードオフだな。危険だけど大連鎖の爽快感を楽しみたいなら ACL2 のほうがいいけど、緻密にかつ安全に進みたいなら Cubical Agda のほうが良いという感じ。


---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:12:33)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。