Slightly changed serialization format.

printf's %a was too fragile to serialize floats and doubles, as it was
behaving differently on different OSes and OS versions. Instead, a hex
representation of the float/double in big endian is used now. While this
is less readable, it is guaranteed to be accurate and always the same.