But these are reals, not floats. With reals, commutativity holds, even though for ieee754 floats it does not.
There's nothing forcing an implementation to calculate (2*6)/3 or (2/3)*6 using binary floats rather than some other method that it can guarantee will give a correct result. These are implementation details, which the grammar doesn't concern itself with. An analyzer could easily discover that the ultimate destination of the calculation is an unsigned integer, and rejig the calculation as necessary to produce the expected integer result (or produce a no-match expression if the result of the calculation would violate the unsigned integer invariant).
Computerized math is hard no matter what you do (rounding, range, precision, overflow behavior, impossible calculations, infinities, etc), and those will still exist whether the grammar prescribes a particular computerized approach or not. So it's better to not force implementation details when you don't have to.
Another thing to consider is that implementations of this metalanguage won't even have to be 100% correct or even handle crazy complex calculations, because real-world data formats won't do such things since they want speed and accuracy in the codecs that don't fall over on platform subtleties. A real world format won't expect the precise bits 00111110100110011001100110011010 (~0.3 in ieee754 binary float 32) for anything, and even if (god forbid) it did, one could just as easily write uint(32,0x3e99999a) instead to make sure there's no mistake (subnormals notwithstanding). You could have provably correct (but slow) implementations, and less-correct-but-super-fast-and-actually-useful-for-the-real-world implementations. A performant implementation might even require for example that calculations whose destination is an integer encoding must be calculable solely using integer math - i.e. (a * b) / c, not (a / c) * b. Nothing wrong with that if it allows you to maximize performance.
On a side note, even the float() function is fraught with subtleties. Different algorithms exist for converting decimal strings to binary floats, which produce subtly different bit patterns depending on the value. We can't get away from that, but once again for the real world it almost never matters because we don't need that level of precision so we just live with it (which is why ieee754 binary has enjoyed such success, and one reason among many why ieee754 decimal is slow to catch on).
The math is pure and should remain pure (especially in the documentation, which this metalanguage is designed for). Making it actually work in silicon is a job for a computer.
There's nothing forcing an implementation to calculate (2*6)/3 or (2/3)*6 using binary floats rather than some other method that it can guarantee will give a correct result. These are implementation details, which the grammar doesn't concern itself with. An analyzer could easily discover that the ultimate destination of the calculation is an unsigned integer, and rejig the calculation as necessary to produce the expected integer result (or produce a no-match expression if the result of the calculation would violate the unsigned integer invariant).
Computerized math is hard no matter what you do (rounding, range, precision, overflow behavior, impossible calculations, infinities, etc), and those will still exist whether the grammar prescribes a particular computerized approach or not. So it's better to not force implementation details when you don't have to.
Another thing to consider is that implementations of this metalanguage won't even have to be 100% correct or even handle crazy complex calculations, because real-world data formats won't do such things since they want speed and accuracy in the codecs that don't fall over on platform subtleties. A real world format won't expect the precise bits 00111110100110011001100110011010 (~0.3 in ieee754 binary float 32) for anything, and even if (god forbid) it did, one could just as easily write uint(32,0x3e99999a) instead to make sure there's no mistake (subnormals notwithstanding). You could have provably correct (but slow) implementations, and less-correct-but-super-fast-and-actually-useful-for-the-real-world implementations. A performant implementation might even require for example that calculations whose destination is an integer encoding must be calculable solely using integer math - i.e. (a * b) / c, not (a / c) * b. Nothing wrong with that if it allows you to maximize performance.
On a side note, even the float() function is fraught with subtleties. Different algorithms exist for converting decimal strings to binary floats, which produce subtly different bit patterns depending on the value. We can't get away from that, but once again for the real world it almost never matters because we don't need that level of precision so we just live with it (which is why ieee754 binary has enjoyed such success, and one reason among many why ieee754 decimal is slow to catch on).
The math is pure and should remain pure (especially in the documentation, which this metalanguage is designed for). Making it actually work in silicon is a job for a computer.