> Python _configuration_ should be changed to disable double rounding on such platforms

That sounds good to me, with the nitpick that setting an x87 FPU to 53-bit precision still doesn't avoid potential double rounding on underflow, and I'm not aware of any easy way to "fix" x87-using code to avoid double rounding on underflow.

That said, the vast majority of practical applications, including random.choice, math.fsum, dtoa.c, aren't going to be affected by double rounding on underflow, so it should only rear its ugly head in corner cases.

If we do this, can we also persuade Guido to Pronounce that Python implementations assume IEEE 754 format and semantics for floating-point?