Post #1415174
2026-04-17 11:22 UTC
I find the proposed agda contributors policy to be quite disappointing. I'm not sure what I will do about this yet, and I'm not actively using Agda at the moment so i don't need to come to a decision now, but I'm leaning towards avoiding Agda as I currently avoid Lean (despite the fact that I like Lean quite a lot as a language, the dreaded bots have infected too much of its ecosystem and culture for me to have a good time engaging with it)
Replies (4)
-
@liamoc@types.pl 2026-04-19 12:08
@mio i call llms and other generative AI tools the "dreaded bots"
-
@liamoc@types.pl 2026-04-19 12:10
@mio it's in a pull request, but mostly it's in the context of several issues trying to hash this out. Many people wanted to ban LLM contributions entirely, but out of deference to specific senior members of the dev team who had a different opinion, a completely non-committal policy was instead adopted.
-
@mio@shrimp.mio19.uk 2026-04-19 12:03
@liamoc What are the dreaded bots? Are they something powered by generative models?
-
@mio@shrimp.mio19.uk 2026-04-19 12:06
@liamoc Where can I read the proposed agda contributors policy? I am unable to find it by using search engines