I assume that for 32-bit floats, you could mostly do away with the HP stuff and just use 64-bit floats, right? Though it does make me wonder if that's always faster than two 32-bit floats. I would think so.
It should be faster to replace the HP numbers entirely with 64-bit floats. Regardless, I think it would be a useful for two purposes: 1) it would serve as an implementation for chips with only 32-bit floats (maybe some kinds of embedded systems) and 2) we can exhaustively test and verify that the algorithm works on all 32-bit numbers, providing more confidence in the 64-bit version.