string <-> float conversions;  this makes sure that the result of the round
operation is correctly rounded, and hence displays nicely using the new float
repr.