> Floating point numbers give you that, problem solved.
No. For example, floating point addition is not necessarily associative. In that sense, floating point numbers aren't even a field and it's wrong to say that they can be used as a stand-in for real numbers.
Floating-point numbers are incredibly useful and it is amazing that we can exactly analyze their error bounds, but it's wrong to treat them as if they were real numbers.
The distinction is irrelevant in the context of computers.
> By contrast, you won't be able to construct a type that encodes exactly the set of real numbers.
You don't need to encode exactly, just like you don't need to encode the integers "exactly".
All you need is a way to guarantee a finite number of significant digits in your real number approximation.
Floating point numbers give you that, problem solved.