[tlaplus] Request for comment: LLM contribution policy

The past few weeks have suggested that the TLA+ project needs a LLM contribution policy. I have a draft PR open for the TLAPM repo on which I would welcome your feedback: https://github.com/tlaplus/tlapm/pull/264

Basic outline is that all design-level discussion (TLA+ mailing list, issues, PRs, community meeting, etc.) must be mediated by humans. I have to read enough slop at my day job where I'm paid to do it and don't want to do it in open source, where I derive happiness from interacting with you all!

For actual code contributions we can follow the Linux kernel policy where AI assistance is allowed, the code is subject to the same standards as anything else, and LLM usage must be disclosed in a git commit trailer (down to specific model version): https://github.com/torvalds/linux/blob/254f49634ee16a731174d2ae34bc50bd5f45e731/Documentation/process/coding-assistants.rst

My actual personal opinion is that we shouldn't use LLM-generated code at all for development on the core tools, as our true goal should be to improve our understanding of how the tools work in the minds of the humans who work on them. Reviewing a LLM-generated PR does not give the same understanding as writing the code yourself. I think this would manifest as a short-term boost in feature & bug work throughput at the cost of reducing the ability for humans to contribute to the tools in the longer term.

Andrew Helwer