Existence of unknowable algorithms ? Here by «algorithm» I mean a (halting) Turing machine with finite alphabet and memory.
Is it possible to obtain by purely existential (i.e. non-constructive) means the existence of an algorithm performing some required task, while beeing unable to explicit it (i.e. write it down or describe it constructively) ?
I hope the question is neither too vague nor too ill-posed, as I'm not so acquainted with these concepts! Thank you for any insight on the matter, feel free to retag or plainly close this naïve question if necessary.
Edit: in view of the answers given so far I think I can better explain what I meant originally. My question is more along the lines of
Is there a task for which an algorithm is known to exist while at the same time it is not possible to recognize the said algorithm?
By this I mean that our innability to perform the recognition is not a consequence of our current lack of actual knowledge, but of an intrinsec formal impossibility to do so. In other word working out that any algorithm outputs what is expected by the task is undecidable by inspection of its content.
(Final) edit: I thank everybody who took the pain to answer my rookie's question... I would like to formulate some comments regarding the (legitimate) objections that has been raised. First we may assume that the formal system is ZFC, in order to fix ideas.
My question was not about "mass problems" (although the examples presented below really are interesting), I was rather asking about a specific task, so it relates more to undecidability problems, as was pointed out by Mark Sapir.
Actually MyFavouriteProblem concerns effective computability of holomorphic dynamical systems satisfying MyFavoriteProperty, which were known to exists by some "abstract" argument and for which I gave a more "constructive" proof. It is doubtlessly a practical improvement (my PC can do the computing), but I wanted to know if from a theoretical point of view some progress really has been made (actually to settle a friendly argument with a colleague of mine).
So the starting point to this question lies in algorithms performing computations with arbitrary floating-point precision on complex numbers, understood as Taylor coefficients of  power series (needs some infinite memory here, I'm afraid, but I don't think it really matters).

*

*Regarding Joel's answer: this argument would be a striking satisfactory answer if it is proved that knowing the value of $N$ is indecidable in ZFC. Maybe one can work out an example where $\pi$ is replaced by some other real number.


*Regarding Goldstern's answer (and subsequent comment/answers): I don't so much think that the argument is a cheat than it does not answer my edited question (edit made after the initial answer). My point is the following. Either some open question $Q$ is decidable in ZFC, in which case we all agree that the program "Yes" or the program "No" answers $Q$, but by inspection of the programs we can decide which one performs the required task once we know which answer is a fact, which is not a formal issue anymore. Either $Q$ is indecidable in ZFC and we cannot prove, in ZFC, the existence of an algorithm answering it (though I'm not sure of this part of my argument). Now if we attach $Q$ to our axioms set then we are back to the previous case, were answering $Q$ has become explicitely tautological. So I believe Goldstern's example does not meet the requirement of my question.


*Timothy's answer is great since it offers a very nice comprehensive summary of the issue as I perceive it. If the unofficial answer to my question is that pessimistic statement, then let it be. The sloppy mathematician in me is perfectly happy with matters as they are ;)
To conclude, I think I should accept Peter Shor's answer, since he gives an example which, as I understand it, answers my query. I'll do that in a little while.
 A: Here is a pure existence proof of computability, where we show that a function is computable, not by exhibiting an explicit algorithm, but by providing a list of infinitely many algorithms, and proving that one of them computes the function; we just don't know which one. 
(This answer is adapted from an answer I gave to Hans Stricker's question Non-constructive proofs of decidability?)
Let $f(n)=1$, if there are $n$ consecutive $7$s somewhere in the decimal expansion of $\pi$, and $f(n)=0$ otherwise. Is this a computable function? 
Perhaps we might try naively to compute it like this: on input $n$, start to enumerate the digits of $\pi$, and look for $n$ consecutive $7$s. If found, then output $1$. But then we realize, of course: what if on a particular input, you have searched for 10 years, and still not found the instance? We don't seem justified in outputting $0$ quite yet, since perhaps we might still find the consecutive $1$s by searching a bit more.
Nevertheless, we can prove that the function is computable by a pure  existence proof. Namely, either there are arbitrarily long strings of $7$s in $\pi$ or there is a longest string of $7$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 $n\leq N$ and value $0$ for $n\gt 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. 
A: The question is a little vague but here is the answer to one possible interpretation of it. Let $R$ be a finite group presentation with finite generating set $X$, $u$ is a word in $X$. Suppose  $G$ is generated by $X$, and finite, then we there is an algorithm to find out if $u=1$ in $X$ (the word problem in every finite group is decidable). But there is no way we can know if there exists a universal algorithm that given $R$ and $u$ tells if $u=1$ in every finite group generated by $X$ that satisfies $R$ (i.e. the uniform word problem in finite groups is undecidable, see 
Slobodskoĭ, A. M. Undecidability of the universal theory of finite groups.
Algebra i Logika 20 (1981), no. 2, 207–230). In fact that situation is quite normal. Decidability of a mass problem means an algorithm to solve it exist, but often it is a pure existence statement.  
A: If you are still not satisfied with any of the current answers, then I think the trouble is that you have not thought through clearly in your own mind what it means for it to be impossible to know some particular mathematical fact.
The first condition that you want to be satisfied is clear enough.  You want it to be provably true that

There exists some Turing machine that solves My Favorite Problem.

Since Turing machines can be enumerated, this is equivalent to saying that we can prove that at least one of the statements in the following list is true.

Turing machine 1 solves My Favorite Problem.Turing machine 2 solves My Favorite Problem.Turing machine 3 solves My Favorite Problem.Turing machine 4 solves My Favorite Problem.$\vdots$

The second condition that you want to be satisfied is that not only do we currently not know any particular statement in this list to be true, but there should be some "intrinsic formal impossibility" preventing us from ever knowing it.
The trouble is that it's not clear what you mean by "an intrinsic formal impossibility."  Suppose for example that Turing machine 314159 happens to solve My Favorite Problem.  What's to stop someone from just baldly asserting, "I know that Turing machine 314159 solves My Favorite Problem"?  Well, of course, being mathematicians, we object to people making such an assertion unless they can prove it.  So probably you want your second condition to look something like this:

For every n such that Turing machine n solves My Favorite Problem, it is impossible to prove that Turing machine n solves My Favorite Problem.

Now the trouble with this statement as it stands is that it is not entirely formal, because we have not specified the axioms we are allowed to appeal to in our proof.  In "ordinary mathematical life," we normally do not bother explicitly saying what axioms we allow.  As trained mathematicians, we recognize a valid proof when we see it and that's good enough for ordinary mathematical work.  However, once you start trying to make statements about the impossibility of proving something, you can't get away with this sloppiness any more.  You have to specify some set of axioms.  Otherwise, there's no way to stop someone from taking "Turing machine 314159 solves My Favorite Problem" as an axiom.
O.K., so we have to specify some set of axioms.  So how about ZFC, everybody's favorite whipping boy?  That's a reasonable choice.  However, as Andreas Blass pointed out in the comments, once you fix a set of axioms, then something like Goldstern's answer works.  Now of course Goldstern's answer seems like a cheat.  We wouldn't want to be accused of cheating, would we?  Of course not.  So, let's choose some other set of axioms.  Whoops, no good…any reasonable set of axioms will leave some statement undecided, and Goldstern's cheat slips in the door.  Dang it, there must be some way to phrase the question so that no cheating answer is possible.  Mustn't there?
I don't think there is.  As soon as you find yourself dealing with one specific statement such as "Turing machine 314159 solves My Favorite Problem," there's no way to avoid this kind of "cheat" when it comes to saying what it means for it to be impossible to prove it.
The only other avenue I see for you to try is this: Instead of saying that for every n it is impossible to prove that Turing machine n solves My Favorite Problem, you could try asking this:

There is no algorithm that, given n, decides whether Turing machine n solves My Favorite Problem.

Ah!  That sounds more like it!  Or does it?  The trouble is, you can choose just about any algorithmic problem you like and it will be undecidable whether Turing machine n solves it.  This is Rice's theorem.  So this isn't really what you want either, since it has nothing to do with the inscrutable structure of My Favorite Problem; it rather has to do with the inscrutability of Turing machines in general.
At the end of the day, I think you just have to accept the uncomfortable fact that there is no way to get an answer that is better than the ones that have been proposed already.  There are problems for which we can currently prove that there is an algorithm but we don't know any algorithm yet, and we can prove that there is no general procedure for turning existence proofs of algorithms into constructive proofs, but if you try to push harder and ask for an explicit example of My Favorite Problem for which an algorithm is intrinsically unknowable, then you're inevitably going to run into the above difficulties.
A: The Robertson-Seymour graph minor theorem shows that membership in any given minor-closed family of graphs can be checked in polynomial time.  It even shows this can be done in $\mathcal{O}(n^3)$ time, but gives no bound on the size of the hidden constant.
A: Yes.
We take a fixed diophantine equation in variables $y,x_1, x_2, \ldots, x_k$.
Task: for an input $n \in \mathbb{Z}$, output either


*

*Five values of $y$ for which solutions exist to the equation.

*A solution to the equation for which $y=n$. 

*"No", in which case there must be no solution with $y=n$.


It is clear that for any diophantine equation, there is a program which performs this task. If there are five values of $y$ for which solutions exist, you need only have the program output these for all inputs. If there are fewer than four values of $y$ for which solutions exist, once you know the solutions, then writing the program is trivial. 
However, telling whether a solution exists to a diophantine equation is undecidable. 
A: Take any open question Q.  ("Is the Riemann hypothesis true"?  "Is P=NP?" etc) 
There is an algorithm that will answer Q correctly. 
It is trivial to prove (in classical logic) that one of the following programs works: 


*

*Program 1:  Print "yes".

*Program 2:  Print "no".

A: Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?
Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:


*

*Given $x$, search for a proof of the form $p(x) = y$.

*When such a proof is found, output $y$.


However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.
Let $p$ be a function that following function:
$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ if its negation holds.
For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following algorithms does the trick:


*

*Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.

*Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.


However, there is no particular turing machine $M$ which ZFC can proof computes $p$. If it did, then ZFC + CH would prove that the inconsistency of ZFC implies there is some $x$ for which $M(x) = 1$. Since this is an arithmetical statement, ZFC + $\lnot$CH also proves it. It also proves that there is no $x$ for which $M(x) = 1$. Therefore, it can conclude that ZFC is consistient. This violates the fact that ZFC and ZFC + $\lnot$CH are equiconsistient. So there is no $M$ that ZFC claims can compute $p$.
So:


*

*ZFC proves $p(x) = 0$ for all numerals $x$.

*ZFC proves $p$ is total.

*ZFC proves $p$ is computable.

*There is no turing machine $M$ that ZFC proves computes $p$.


So I guess an algorithm for $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).
A: I've already written an answer but in light of the "final edit" to the question, I believe that something more can be said.  In particular, I want to address the following comment.

Actually MyFavouriteProblem concerns effective computability of holomorphic dynamical systems satisfying MyFavoriteProperty, which were known to exists by some "abstract" argument and for which I gave a more "constructive" proof. It is doubtlessly a practical improvement (my PC can do the computing), but I wanted to know if from a theoretical point of view some progress really has been made.

If I read this correctly, the previous proof showed that the problem was algorithmically decidable (in some model of real computation that allows manipulation of infinite-precision real numbers).  If this is the case then there are (at least) two ways in which your new algorithm can be regarded as making "theoretical" progress.


*

*It could be a situation like the Robertson–Seymour graph minor theorem mentioned in Noah Stein's answer.  Here there is a whole family of computational problems, and the theory proves that every member of the family is solvable in polynomial time; however, for any particular member of the family, there may be no known polynomial-time algorithm, since the theory does not yield an effective algorithm for finding the polynomial-time algorithm.  Finding an explicit algorithm for a particular member of the family for which an explicit algorithm was not known would count as theoretical progress in anyone's book.  This sort of situation is rare, so I suspect that your case is not of this type, but if it is, it would be very interesting!

*The earlier proof might have yielded an explicit algorithm in principle if you were willing to unpack the argument, but the computational complexity would have been horrendous.  Your proof yields a vastly superior computational complexity.  Some old-style mathematicians might not regard this as "theoretical" progress, but I think the dominant viewpoint nowadays is that improvements in computational complexity count as theoretical progress and not just practical progress.  Indeed, computational improvements often provide a convenient yardstick for measuring theoretical progress: Your new proof surely uses new ideas, and the fact that it gives a better algorithm is a clear demonstration of the value of the new ideas.  As other examples, Gowers's new proof of Szemerédi's theorem or Folsom, Kent, and Ono's new formula for the partition function come to mind.  The value of the new ideas was obvious to experts, but even non-experts could tell that something major had happened because of the vast computational improvements that were obtained.
A: In the paper Towards the equivalence of breaking the Diffie-Hellman protocol and computing discrete logarithms from Crypto'94, Ueli Maurer "showed" how to compute discrete logarithms efficiently given an oracle for the computational Diffie-Hellman problem (given elements $x=g^a$ and $y=g^b$ compute $g^{a*b}$).
His algorithm requires the knowledge of an elliptic curve of smooth order, which is conjectured to exist, but no efficient way of finding it is known.
