You could probably restrict to rational numbers, and still verify? Languages like Python, Haskell, Rust etc have good support for arbitrary length rational numbers.

Each floating point number is also a rational number, and thus you could then restrict again to floating point afterwards.