Sorry if this is another crank finitism question, I am bit confused.
According to wikipedia:
Constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists....
In constructive mathematics, one way to construct a real number is as a function $f$ that takes a positive integer $n$ and outputs a rational $f(n)$, together with a function $g$ that takes a positive integer $n$ and outputs a positive integer $g(n)$ such that...
Blah blah blah, this is basically using the same idea behind limits of Cauchy sequences except with the requirement that the limit must be computable. In other words, constructivism only allows us to construct computable real numbers, which makes sense of course. Wikipedia gives an example:
Under this definition, a simple representation of the real number e is: ${\displaystyle f(n)=\sum _{i=0}^{n}{1 \over i!},\quad g(n)=n.}$
However what I can't understand is the justification of the functions $f$ and $g$ in the first place. Sure both of them are computable, but they aren't constructive! The domain of both $f$ and $g$ is the set of natural numbers. And the set of naturals is an infinite set. Therefore it requires the axiom of infinity to be constructed.
But the axiom of infinity is not a constructive axiom! The axiom of infinity asserts the existence of a special set with some given property. But that's not allowed in constructivism. Constructivism would require us to find an terminating algorithm that constructs the special set.
But without the axiom of infinity, infinite sets cannot be defined at all, therefore we can't construct the set of naturals, therefore we can't construct the functions $f$ and $g$ from the example given by wikipedia above. So the above "example" is moot. It's not valid.
And therefore the computable numbers can't be defined constructively. I do not see how to work around this technicality.
This seems to me like a semantic issue: Nowadays, after the advent of the absolute infinite in mathematics, the axiom of infinity has begun being conventionally interpreted to posit the existence of infinite totalities, whole and complete. But this is not the only possible interpretation. An alternative is that it asserts the existence of an inhabited species such that it is always possible to construct an element of it that is distinct from all other elements that have been constructed thus far. Here, I call it "species" instead of "set" to punctuate that we're looking at it quite literally like any species of animals: We know criteria by which to identify members of them, but at any point we have not seen all of them. The difference is that in the animal analogy, there is an external world that at any moment comprises a fixed number of animals of a given species, but in constructive mathematics we construct every mathematical object, and furthermore we start from somewhere, so at any point we have finitely many mathematical objects. It's just that with the natural numbers, we can always "find" or make newer ones that we hadn't seen before—at least ideally.
(Also note how the axiom stays exactly the same, but its interpretation is the one that determines whether it's possible to satisfy it in principle. This was the original controversy around the axiom of choice: Not that it was inherently nonconstructive, but that the conventional interpretation was nonconstructive—this puts it highly anachronistically, but it's arguably the gist of the problem and also how it was solved. It is now known that under different interpretations, or different models, the axiom may or may not be satisfied.)
As for functions whose domains are that of the naturals, it works similarly. In frameworks like ZF, a function is also a set, and if one interprets sets as complete totalities, arbitrary functions with the domain of naturals will also be some "absolute infinity", or rather a relation of possibly infinite complexity between two sets. In the "species" interpretation, this is not the case: A function $f$ from species $A$ to species $B$ is a rule, such that at any point if you admit any object $x$ into $A$, by applying the rule to $x$ you can obtain (construct) an object $f(x)$ that will be admitted to $B$. Moreover, if you deem equal any two objects $x$ and $x'$ of species $A$, then the corresponding objects $f(x)$ and $f(x')$ in $B$ will be deemed equal as well. Of course, interpretations vary—in particular, the strictures put on the word "rule" in the previous sentence have very interesting discussions surrounding them. But the gist is largely the same; you don't need to know every element of $A$ to verify whether $f$ is a function. At the very least, the function will be a relation of indefinitely growing complexity, but at any given point the complexity is finite. Debates over what "rule" means, in constructive/finitistic contexts, usually boil down to how fast this complexity should be allowed to grow until it shouldn't be considered a well formed function anymore.
As for formally practicing constructivism, there are many formal systems that admit readily constructive interpretations. But they will differ in how they encode the idea of a function. For instance, as I mentioned, in pure set theories functions will inevitably be sets, likely encoded as formal "lookup tables" of sorts. In type theories, functions will be elements of certain product types, where it is possible to formally apply them and then compute the resulting expression. In systems motivated by category theory or topos theory, functions may be primitive and left undefined.