On: Pointers Are Complicated II, or: We need better la...

[Dylan16807]

I count the definitions given for a proof as part of the proof.

[thaumasiotes → Dylan16807]

That is a serious mistake here, where the definition of a correct optimization is of significantly more interest than the result that they can be composed. We want to apply optimizations alone even more than we want to apply them together.

Putting things another way, this definition is clearly not given as part of a proof; it is given for its own sake, and the proof uses it.

[Dylan16807 → thaumasiotes]

I wouldn't call slightly imprecise wording a "serious mistake".

I object to points at the part of the post. My objections are unchanged by what we call it.