浮動小数点数の計算には丸め誤差やその他の誤差が付き物ですが、同時に意外にも正しく計算してくれる場合があることに驚かされます。
"Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number"にもそのようなケースが紹介されています。すなわち、浮動小数点数の2乗の平方根は(2乗したときにオーバーフローやアンダーフローが起こらない限り)丸めに関わらず元の数の絶対値になる、というものです。基数が2であり、precisionが1より大きいという仮定のもとで、Coqを用いて形式的に証明されています。
具体例として、IEEE 754において既定の丸めモード(round to nearest, ties to even)にしたがってfloat(binary32)やdouble(binary64)で計算する場合などが当てはまります。
参考文献に挙げられている"Mathematics Written in Sand"に同様の記述が見えることから、この事実は30年以上前から知られていたようです。