I think that the heart of the question is "Can one give a rigorous meaning to 'there is no constructive proof to the Peano's theorem'?" The answer to this is yes, but the answer is not as simple as one might naively hope.

The way that one would give an affirmative answer is to first choose a constructive framework. The proof will not show that there is no constructive proof in *any* possible sense, only that there is no constructive proof *within that framework*. However, if the framework is sufficiently natural, then the negative answer in that framework will often be viewed as somewhat definitive.

Once a particular framework has been chosen, if one can show that the theorem implies, within the framework, some principle that is known to be unprovable in the framework, then the theorem itself is certainly unprovable by any means that can be formalized within the framework. One such principle might be the law of the excluded middle, but there are many weaker but still nonconstructive principles that are also used in practice.

There are several frameworks for constructive mathematics; an old but excellent introduction is *Varieties of Constructive Mathematics* by Bridges and Richman (1987).

Two particular frameworks worth mentioning are:

Bishop's framework, which is presented in Bishop and Bridges, *Constructive Analysis*, 1985. Briefly put, this framework was intended to resemble ordinary informal mathematics (but with special care to avoid nonconstructive methods, and other issues of classical mathematics that Bishop felt obstructed constructive proofs).

The "Markov-type" framework, developed by many constructivists but particularly associated with Russian constructivism. Briefly put, this framework focuses on algorithms, rather than more abstract mathematical objects. To have an object is to have an algorithm for it.

It appears that the answer in both of these frameworks is that there is no constructive proof of Peano's theorem.

Aberth (1971) showed that Peano's theorem fails in a Markov-type setting (full text available from the journal page). Reference: Oliver Aberth, The failure in computable analysis of a classical existence theorem for differential equations, Proc. Amer. Math. Soc. 30 (1971), 151-156. MR 302982

Bridges (2012) showed that, in a Bishop-type setting, Peano's theorem implies the principle LLPO, which is a well-known non-constructive principle used to gauge the non-constructivity of theorems. Reference: Bridges, Douglas S.,
Constructive solutions of ordinary differential equations. Logic, construction, computation, 67–77, Ontos Math. Log., 3, Ontos Verlag, Heusenstamm, 2012. MR 3204972

It was pointed out in the comments that, in the context of classical Reverse Mathematics, Peano's theorem is known to imply the system $\mathsf{WKL}_0$. That is a clue that the theorem may not be constructive, but there are two issues that prevent it from being definitive. First, the implication proof may require non-constructive methods. Second, the system $\mathsf{WKL}_0$ is tightly tied to Bishop's program for constructive analysis, and some theorems that are equivalent to $\mathsf{WKL}_0$ in the context of Reverse Mathematics are nonetheless considered constructive by Bishop, due to the difference between the Reverse Mathematics framework and Bishop's framework. However, the two references above are both written in constructive frameworks, and I would view them as definitive.

Subsystems of Second Order Arithmetic. From that result we can also see that Ascoli's theorem is not required, since that is equivalent to the stronger axiom of arithmetical comprehension. $\endgroup$