Example of an algorithm that lacks a proof of correctness

We have Hoare logic. Why is it still possible that an algorithm is right but there is no proof that it's correct? Suppose the algorithm is expressed in C. Then we can argue step by step that it's doing what it's supposed to do.

So my question is:

Give me an example of an algorithm that's right but does not have a proof of correctness.

EDIT: I think a little background can help clarify where I'm going. Let me quote Scott Aaronson:

Since the 1970s, there's been speculation that P $\ne$ NP might be independent (that is, neither provable nor disprovable) from the standard axiom systems for mathematics, such as Zermelo-Fraenkel set theory. To be clear, this would mean that either

-
a polynomial-time algorithm for NP-complete problems doesn't exist, but we can never prove it (at least not in our usual formal systems), or else

-
a polynomial-time algorithm for NP-complete problems does exist, but either we can never prove that it works, or we can never prove that it halts in polynomial time.

I'm referring to the second possibility. Since Aaronson can so confidently list it as a possibility, I think there must be an existing example of type 2. That's why I'm asking this question. But it seems a quick and clear answer is not in view.

Here is an algorithm for the identity function:

• Input: $n$

• Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$

• Otherwise, output $n$

Most people suspect this algorithm computes the identity function, but we don't know, and we can't prove it in the commonly accepted framework for mathematics, ZFC.

StackExchange Computer Science Q#69580, answer score: 51