lo.logic - Non-constructive proofs of decidability?

When I teach computability, I usually use the following example to illustrate the point.

Let $f(n)=1$, if there are $n$ consecutive $1$s somewhere in the decimal expansion of $pi$, and $f(n)=0$ otherwise. Is this a computable function?

Some students might try naively to compute it like this: on input $n$, start to enumerate the digits of $pi$, and look for $n$ consecutive $1$s. If found, then output $1$. But then they realize: what if on a particular input, you have searched for 10 years, and still not found the instance? You don't seem justified in outputting $0$ quite yet, since perhaps you might find the consecutive $1$s by searching a bit more.

Nevertheless, we can prove that the function is computable as follows. Either there are arbitrarily long strings of $1$ in $pi$ or there is a longest string of $1$s of some length $N$. In the former case, the function $f$ is the constant $1$ function, which is definitely computable. In the latter case, $f$ is the function with value $1$ for all input $nlt N$ and value $0$ for $ngeq N$, which for any fixed $N$ is also a computable function.

So we have proved that $f$ is computable in effect by providing an infinite list of programs and proving that one of them computes $f$, but we don't know which one exactly. Indeed, I believe it is an open question of number theory which case is the right one. In this sense, this example has a resemblence to Gerhard's examples.