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

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.