alt Hacker NewsYes, the idea of a turn [1] is interesting. And maybe useful.
I have a different question: What would it take for a compiler to remove (elide) the multiply by pi + divide by pi that the author uses as an example? I guess one would not have to go as far as a Lean proof that two bits of code produce the same result?
Replies
The short answer is you need fast-math flags to allow optimizations that may change floating-point results, and you also need to guarantee an implementation of sinpi/cospi (these were added in C23, so they're not all that common in host library implementations yet).
It's possible if you had the implementation of the math library visible to the compiler that it could do inlining and then simplify expressions, but honestly most math library function implementations are going to be the kind of function that doesn't get picked up by inline heuristics, as there's a pile of if statements (handling special cases and range reduction) that the compiler can't eliminate due to there not really existing a sufficiently powerful FP range analysis.
Well, they don't produce the same result in floating point math, I'm afraid.
So you'd need to teach your compiler about what your formulas mean and what context you are using them in. (Ie are you actually doing geometry, or is your AI coding agent just trying arbitrary activation functions for your neuronal net experiments and some of them happen to look like geometry?)