Post #1101303
2026-03-02 13:16 UTC
@mevenlennonbertrand well at least with Agda you probably don't need to burn as many GPU cycles to find a proof of false, so you could consider it to be more ecological alternative.
Replies (2)
-
@mevenlennonbertrand@lipn.info 2026-03-02 13:38
@jesper@agda.club Yeah, I don't want to translate "9€ of Claude tokens" in kgs of CO2...
-
@dysfun@social.treehouse.systems 2026-03-02 13:18
@jesper@agda.club @mevenlennonbertrand@lipn.info believe_me in idris is only 10 chars. we've got you nailed on this rather unusual benchmark.