Post #2326689

2026-04-23 13:06 UTC

@de_Jong_Tom@mathstodon.xyz @gadmm@mathstodon.xyz My understanding is that some of the core Agda devs who do extremely valuable but super tedious development want to be able to use AI to ease that burden. Which doesn't sound so bad, until you dig deeper into what "using AI" entails.

Replies (1)

@gadmm@mathstodon.xyz 2026-04-24 18:08

@JacquesC2@types.pl @de_Jong_Tom@mathstodon.xyz To clarify my question, I am interested in it from a point of view of governance of commons. - If someone opens a PR containing LLM-generated code, can it be closed as a consequence of people reminding that “there is no consensus in accepting LLM-generated code”? - If someone proposes a PR that adds a section to CONTRIBUTING.md informing that “there is no consensus in allowing LLM-generated code”, will it be accepted? I'd very naively expect the answer to be yes to both according to the reasoning used. In any case seeing this opposition by many people reflects well on the #agda community in my opinion. When #ocaml adopted a lukewarm policy, few people paid attention (apart from people with ties to Jane Street for some reason). The discussion did not focus on the ethical issues whereas the legal issues were sidestepped the way those policies usually do.

Open ##2326690