Are there non-constructive algorithm existence proofs? I remember I might have encountered references to problems that have been proven to be solvable with a particular complexity, but with no known algorithm to actually reach this complexity.

I struggle wrapping my mind around how this can be the case; how a non-constructive proof for the existence of an algorithm would look like.

Do there actually exist such problems? Do they have a lot of practical value?
Consider the function (taken from here)

$\qquad \displaystyle f(n) = \begin{cases} 1 &amp; 0^n \text{ occurs in the decimal representation of } \pi \\ 0 &amp; \text{else}\end{cases}$

Despite the looks, $f$ is computable by the following argument. Either


$0^n$ occurs for every $n$ or
there is a $k$ so that $0^k$ occurs but $0^{k+1}$ does not.


We do not know which it is (yet), but we know that $f \in F = \{f_\infty, f_0, f_1, \dots \}$ with


$f_\infty(n) = 1$ and
$f_k(n) = [n \leq k]$.


Since $F \subset \mathsf{RE}$, $f$ is computable -- but we can not say what  $f$ is.