> define a function f in some programming language to be a real if it can be proven from a specific set of axioms that... Fine, but these programs only compris

> define a function f in some programming language to be a real if it can be proven from a specific set of axioms that... Fine, but these programs only comprise constructive reals. Similarly, with my choice of Real := Nat -> Digit, there are only countably many functions you could actually (create a process to) write down which inhabit that type, but that doesn't make the type countable. There are at most countably many programs one can access in any type. This follows from what programs are: finite (though arbitrarily long) strings over a finite alphabet. That doesn't refute other interesting properties about the "sizes" of these things, as given by the existence or non-existence of certain maps into and out of other types.