@dysfun@social.treehouse.systems
Post #1582554
2026-04-16 21:57 UTC
@agentultra if you can live with the limitations as a proof assistant, idris is quite excellent for dependently typed programming. and realistically you should know if you encode girard's paradox or so.
Replies (1)
-
@agentultra@types.pl 2026-04-16 21:59
@dysfun sometimes I like to encode paradoxes on purpose. Calculate one more byte of the Planck constant. Just to see if any extra-dimensional entities are listening and available for a little summoning party.