> And besides, I'm guessing you could replace ℝ with T (for Turing) and most of the proofs would go just fine.
This is wrong. LUB doesn't hold for the computable reals, and this means that a lot of classical proofs straight up don't work anymore.
That's not to say you can't build a different kind of real analysis built only on the computable reals, some mathematicians have tried to do similar things in the past, but it's going to be a different framework with not exactly the same theorems and not exactly the same proofs; for example, there are no discontinuous functions anymore.
Yeah, I'm sure there are some holes (poor attempt at a pun), but you already know you can get arbitrarily close to whatever bound with rationals, much less computables, so it seems like someone better educated than me could shore that up.
Anyways, the computables have unfortunate properties too (not knowing if you'll eventually need to carry for addition, or when to stop testing for equality), so I'm left wondering if some genius in the future will come up with a new way to build the numbers which are more satisfying.
This is wrong. LUB doesn't hold for the computable reals, and this means that a lot of classical proofs straight up don't work anymore.
That's not to say you can't build a different kind of real analysis built only on the computable reals, some mathematicians have tried to do similar things in the past, but it's going to be a different framework with not exactly the same theorems and not exactly the same proofs; for example, there are no discontinuous functions anymore.
There's some more discussion here: https://www.reddit.com/r/math/s/LSL487ncag