Is there an algorithm that provably exists although we don't know what it is? In mathematics, there are many existence proofs that are non-constructive, so we know that a certain object exists although we don't know how to find it.

I am looking for similar results in computer science. In particular: is there a problem that we can prove it is decidable without showing an algorithm for it? I.e. we know that it can be solved by an algorithm, but we don't know what the algorithm looks like?
The simplest case I know of an algorithm that exists, though it is not
known which algorithm, concerns finite state automata.

The quotient $L_1/L_2$ of a language $L_1$ by a language $L_2$ is
defined as $L_1/L_2=\{x \mid \exists y\in L_2 \text{ such that } xy\in L_1\}$.

It is easily proved that regular set are closed under quotient by an
arbitrary set.  In other words, if $L_1$ is regular and $L_2$ is arbitrary (not necessarily regular), then $L_1/L_2$ is regular, too.

The proof is quite simple. Let $M=(Q,\Sigma,\delta,q_0,F)$ be a FSA
accepting the regular set $R$, where $Q$ and $F$ are respectively the
set of states and the set of accepting states, and let $L$ be an
arbitrary language. Let $F'=\{q\in Q\mid \exists y\in L \;\;\delta(q,y)\in
F\}$ be the set of states from which a final state can be reached by
accepting a string from $L$.

The automaton $M'=(Q,\Sigma,\delta,q_0,F')$, which differs from $M$
only in its set $F'$ of final states recognizes precisely $R/L$.  (Or see  Hopcroft-Ullman 1979, page 62 for a proof of this fact.)

However, when the set $L$ is not decidable, there may be no algorithm
to decide which states have the property that defines $F'$. So, while
we know that the set $F'$ is a subset of $Q$, we have no algorithm to
determine which subset. Consequently, while we know that $R$ is
accepted by one of $2^{|Q|}$ possible FSA, we do not know which it is.
Though I must confess we know to a large extent what it looks like.

This is an example of what is sometimes called an almost constructive
proof, that is a proof that one of a finite number of answers is the
right one.

I suppose an extension of that could be a proof that one of an
enumerable set of answers is the right one. But I do not know any. Nor
do I know a purely non-constructive proof that some problem is
decidable, for example using only contradiction.