Conversation

Notices

1. Embed this notice
   Ⓑⓡⓔⓣⓣ (brettm@swarm.coiloptic.org)'s status on Friday, 03-Jul-2026 19:10:53 JST Ⓑⓡⓔⓣⓣ
   TIL about functional language Idris2, and refreshingly "contributions that arise from Generative AI or Large Language Models, including contributions made by Autonomous Coding Agents that use 'Agentic Coding', will not be considered"
   
   https://idris-lang.org/
   
   https://github.com/idris-lang/Idris2/blob/main/CONTRIBUTING.md
   
   • Embed this notice
     iced depresso (icedquinn@blob.cat)'s status on Friday, 03-Jul-2026 19:10:51 JST iced depresso

     in reply to
     @brettm i've seen idris a couple of times. one of my mutuals used to be big in to it.
     
     i think Lean is eating up the whole dependently typed space these days
   • Embed this notice
     iced depresso (icedquinn@blob.cat)'s status on Friday, 03-Jul-2026 19:25:57 JST iced depresso

     in reply to
     @brettm i'm not a neverclanker :blobcatderpy:
     
     they do have a bandwagon pushing for LLMs to write the proofs, though, which isn't great.
     
     there's some reason why coq and lean don't just make a version of isabelle's sledgehammer tactic. i think its about HOL is ultimately boolean predicates where dependent types are turing complete.
     
     either way, lean compiles to c (via koka's perseus papers), where idris has been around some decade and has never managed to escape the concept compiler stage. i basically can't ship idris, or i probably would have been moved by it backwhen.
   • Embed this notice
     Ⓑⓡⓔⓣⓣ (brettm@swarm.coiloptic.org)'s status on Friday, 03-Jul-2026 19:25:58 JST Ⓑⓡⓔⓣⓣ

     in reply to

     • iced depresso
     @icedquinn@blob.cat i would not personally use it as it does accept ai contributions, also seems heavily involved with ai companies
     
     https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md