[mihaild]

For example, algorithm that just copies it's input to output, unless input is proof of inconsistency of arithmetic, is correct algorithm to calculate function f(x) = x - yet it's unprovable in PA that it's correct.