A single uncertainty bit just isn’t enough. If one is going to go that route, representing real numbers faithfully, then one probably wants (exponential) continued fractions (CFs) instead, because they have much better computational properties:

• CFs are stored as lists of integer coefficients, and can be expressed as iterators which yield integers one at a time
• CFs exactly cover the real numbers
• CFs can, with one extra bit, exactly store not just the rational numbers but all quadratic surds
• CFs can, with an extra zero/infinity coefficient, express whether they are finite (equality is still undecideable, of course)
• CFs can be truncated simply by taking a prefix of the list of coefficients, and these truncations are extremely good
• CFs can represent numerous transcendental constants exactly as infinite iterators

But note that, ultimately, the reason that they went with their custom type is so that they could embed the decideability of RCF into a slightly-richer but still-decideable theory. Unums couldn’t do this at all; they’re quite numeric.

Unums are briefly referenced actually:

Hardware-architecture-level alternatives to conventional machine floating point arithmetic have occasionally been proposed (for example [22, 23]). These address problems orthogonal to our concerns.

[22] is Gustafson’s Beating Floating Point at its Own Game: Posit Arithmetic which describes posits and unums.

By the way: for those that prefer slides, there’s also a YouTube video with an overview of the paper.