[yellowflash]

Can't we just produce a function from Nat -> 0|1|2|3..9? Which in effect can represent reals?

Though addition might not be defined on some of the reals, if represent it like that.

But Proof checkers like lean/coq all use Cauchy sequences to represent reals. So they are in effect constructible.

[aeneasmackenzie]

You can easily do so (usually not that specific representation) but there "are" more reals in the classical construction than you can represent with computations. Constructive mathematics just lets you say "No, this is all of them."

[yellowflash]

It never says, its all of them (Sort of LEM is working in all of them). It just says, thats all you can work with.

[aeneasmackenzie]

It's all of them. You can't give an example of a real number that's not computable.

[Dylan16807]

Chaitin's omega number? I can give you an exact but incomplete equation for it, and tell you how it starts. Not every non-computable number is "pretend you could choose a random normal number, somehow".

I'm not sure if this answer is relevant, but might as well mention it.