Post #2326690
2026-04-24 18:08 UTC
@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.
Replies (1)
-
@JacquesC2@types.pl 2026-04-24 19:30
@gadmm@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz My best understanding is that the answer to 1. is "it depends" (!!!) and 2. is "probably". However some of the very anti-LLM people have left [very sad, given the community is quite small], so I'm not sure exactly how that changes things. Before the "it can be allowed" decision, some LLM code (by old timers) was allowed, and some LLM code (huge, by new people) was rejected. The situation is extremely muddy.