How do proof assistants nowadays avoid floatpoint error?

Question

I heard that Coq is using "Dedekind cut", but how's that related to floatpoint errors?

Can we just use something like

data Q : Type where
  div : N -> N -> Bool -> Q

To replace all usages of floatpoint numbers?

Answer 1

It depends on whether you want to "simply" reason about the properties of real numbers, or if you want to perform actual calculations.

If you want to prove things about their general properties, then using Dedekind cuts is feasible.

If you want to compute actual numerical things, then you need a numerical representation of the cut, and then you're back to some computable representation of (some of) the reals (you can't get all of them). It doesn't strictly have to be floating point numbers - you could use arbitrary precision arithmetic for example - more accurate but slower in general.

Your type however seems to be aiming to represent the Rationals, for which floating point numbers are unnecessary, you could just have a type with one constructor: nat -> nat -> Q.