A programmer’s doubts about countable vs uncountable infinity (A short disclaimer: I'm not a mathematician, and I'm not trying to say anything is "wrong" about these famous proofs. I'm trying to get my bearings and maybe find where I can read more about a certain style of mathematical thinking.)
I’ve seen a few explanations of the proof that there are “more” reals than integers. Here’s one on youtube. It uses Cantor’s diagonal argument. This idea seems roughly equivalent to defining the difference between countable and uncountable infinity.
I still have doubts about this line of thinking. Maybe my confusion is more in the realm of philosophy than math. I have a background in computer programming, and I tend to think of math in terms of what we can make manifest in a running computer program. If something can exist only in thought, I don't value it as much.
Some steps of this proof (as I’ve seen them) go like: "Do X an infinite number of times. When you're done, then do Y". Obviously such a thing can never "happen" in a material world where actions take finite time, nor can it "run" in a computer program.
This kind of infinity seems different from the one I first encountered in calculus, which can be used usefully in a computer program. For example, an "infinitesimal" number in calculus is like a finite number with an attached procedure to generate a smaller number, if needed. The statement "$dx$ is infinitely small" thus translates to "Here's $dx$, lets start with 0.001. If you want something smaller, ask." Again, as a computer programmer I'm used to dealing with values with attached procedures, so this feels natural to me.
If I imagine infinity in this "executable" way, as a source of numbers that can always provide another number, then this diagonal proof doesn't seem to work. You can always generate a new real number that isn't in your list of reals, but the source of integers can always "answer" by providing yet another integer, and the two infinite streams of numbers duel it out for as long as we want.
Questions

*

*Can you define countable vs. uncountable infinity, or prove there are more reals than naturals,  without using one of these un-executable steps that say "do this forever, and when you're done ... “.

*Is there is a school of mathematics that doesn't accept the proof, or that thinks as I describe above? If so, what it is called?

 A: I definitely recommend checking out constructivism for a broader look at what the sort of math you're advocating for looks like, but I think I can hopefully shed a bit of light on how to interpret Cantor's diagonal argument computationally.
1. What is a real number computationally?
Computable reals:
First we need to interpret real numbers as computations. We say that a real number $\alpha \in [0,1)$ is computable if there is a (terminating) algorithm $T$ that given a natural number $n$ as input produces $T(n)=\alpha_n$, the $n$th binary digit of $\alpha$. (We can assume that $\alpha$ is between $0$ and $1$, since the integer part of $\alpha$ can be represented by a natural number and a sign bit).
There are also many other variants that are all essentially equivalent. The idea is that we should be able to approximate the real number to within $\epsilon$ in finite time by a deterministic algorithm.
Other reals: Now, there are things that we might want to consider real numbers that cannot be represented by a finite, deterministic algorithm $T$. For example, if we are given a source of randomness, we could randomly output bits, and there will be no deterministic algorithm that would be guaranteed to replicate the output of the random bit producer for as long as we want. The probability of matching $n$ bits of the random bitstream is $1/2^n$ after all (assuming $P(0)=P(1)=1/2$).
Representing arbitrary reals: So hopefully we can agree that there should be other things we might want to consider real numbers. An "arbitrary" real number can be represented by an oracle for its bits. If we want to use Turing machines as our computation model, an arbitrary real number can be thought of as giving our Turing machine another tape, on which we've written down the entire binary expansion of this real number. For our purposes, I prefer to work at a higher level than Turing machines, so I'll think of an oracle as a black-box function call that instantly returns with the correct answer. So an oracle for a real number's bits is just a function $\omega$ that takes a natural number $n$ and returns a bit $\omega(n)$ representing the $n$th bit of the binary expansion of the corresponding real number.
2. Cantor's argument computationally
How do we want to interpret Cantor's argument computationally?

Assume for each natural number $n$ we have an oracle $\omega_n$ representing a real number.
Then we can (computably) produce a real number from these oracles together with a proof  that the real number we have produced is different from any of the real numbers represented  by the oracles.

The algorithm is straightforward. We define $T(n) = 1-\omega_n(n)$. The proof that $T$ is different from all the $\omega_n$ is that $T(n)\ne \omega_n(n)$, so they can't represent the same real number. (Actually, we have to be careful, because rational numbers have two distinct binary expansions, so this isn't strictly true. We can fix this by working in a base other than 2, or by modifying more than one bit of the number, but that's more of a technical detail.)
3. Interesting side note
Note that even though the computable reals are countable, since there are at most countably many algorithms, the diagonal argument proves that the computable reals are computably uncountable. I mean this in the sense that the diagonal argument proves that no computable list of computable reals can be complete. I.e., if we can write down a procedure that enumerates procedures for computing reals, then Cantor's diagonal argument allows us to write down a computable real that cannot possibly be generated by our enumeration procedure.
