Yes, 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?

[1] https://en.wikipedia.org/wiki/Turn_(angle)

▲

eru an hour ago | parent [-]

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?)

▲

nomel 36 minutes ago | parent [-]

It's a mistake to care about equality of floating point numbers [1]. You must usually consider the lower bits of the number as random.

I assume you're saying something other than this though?

[1] https://en.wikipedia.org/wiki/Machine_epsilon

	▲	ainch 18 minutes ago \| parent \| next [-]
		I think the point is that, from a compiler's perspective, it's not obvious how much you should be allowed to optimise code at the cost of changing the outcomes of floating points maths - do you allow 1e-10, or 1e-6, or 1e-4 level changes? Does your compiler have to run some test calcs to bound the scale of the change introduced by rewriting fp maths? Some compilers will let you opt in to rewriting floating point maths, but that's opt in so users understand that their numeric outputs might change between optimisation levels. For more, there's a good post on this kind of flag in Rust: https://pythonspeed.com/articles/faster-float-math-rust/
	▲	eru 5 minutes ago \| parent \| prev [-]
		Huh, what? Floating point numbers have a standard, you know. They aren't non-deterministic YOLO numbers. By default, the compiler has to stick to what the standard requires, and can't just say add arbitrary imprecision. Your epsilon is what you get when you try to analyse floating point numbers as approximations of real numbers. But they also have an independent life as bit patterns, and the compiler can't just willy-nilly muck around with these bit patterns.