At 30:42 of Norman Wildberger's Difficulties with real numbers as infinite decimals (II) lecture, he raises the question whether "certificates of boundedness" (of the runtime of the algorithm to compute a certain number of digits) should be part of a computable real number.
I thought the answer to that question would be clearly no. However, a similar idea occurs in section "2.2 Numbers as programs" on page 5 of Exact Real Computer Arithmetic with Continued Fractions by Jean Vuillemin, 1987. That paper appears to be quite good and very reasonable otherwise, so now I wonder whether I might be wrong here. Here is the reasoning:
Theorem 1 (Cantor) Let $\mathcal R$ denote the subset of $\mathcal L$-expressions which represent numbers, that is the computable reals expressed as programs in $\mathcal L$.
- The set $\mathcal R$ is denumerable.
- No algorithm can effectively enumerate all the elements of $\mathcal R$.
As equivalent to (2), we see that no algorithm can decide, in finite time, if an arbitrary $\mathcal L$-expression $e$ denotes a number, i.e., $e \in \mathcal R$. Therefore, since we cannot expect the computer to do it for us, we must provide a correctness proof with every real number definition, i.e., program.
My problem is that a correctness proof only makes sense after an axiom system has been specified. And I believe that for any reasonable axiom system, the ("extensional") set of computable real numbers which can be proven correct in that axiom system will be a proper subset of the ("extensional") set of all computable real numbers.
On the other hand, I might be wrong. For example, the ("extensional") set of languages defined by the provably polynomial time algorithms is identical to the ("extensional") set of languages defined by all polynomial time algorithms.