[llvm] [RFC][Uniformity] add proof section uniformity is safe to use across transforms (PR #170628)

[Nicolai Hähnle via llvm-commits]

https://github.com/nhaehnle commented:

I like how you describe what you're trying to do in the PR description. *That* is what is needed in the Introduction sub-section you're adding. As-is, that subsection is just confusing.

I dislike using all this formal language that gives the appearance of a formal proof but then ends with a note that oh BTW, this isn't trying to be a formal proof.

Going into this, I thought what I would get is some guidelines of the form: "if you restrict your transform to doing things X, Y, Z, then you can be confident that it is correct w.r.t. convergence and uniformity". But somehow that's not what I got? Or at least I wasn't able to parse it out.

If you want to continue pursuing this, and I did not misunderstand the goal, then I recommend you focus primarily on giving this sort of guideline. And start with stuff that's simple instead of trying to solve it all at once.

https://github.com/llvm/llvm-project/pull/170628