Not at all. An unprovable statement is, in fact, exactly such a non-computable function. Supposing S is a non-computable function, all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable).
In any rigorous logic it is not. An unprovable statement is a non-existent value whereas the non-computable function is a mapping to a non-existant value. Sure there are ways of turning one into another (however there is not an isomorphism), but that does not make them the same.
> all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable).
As the other comments point out, you can't check just one case. f bar's definition makes it computable at a bunch of functions.
The lecture you linked in the article actually has a follow up where it goes into showing that a formal language would be able to prove any computable function's value. It isn't hard, but it requires some thought.
I need to check my undergrad metalogic notes, but I think they are "almost" the same. You might be right though, it's a very nuanced point you're making. IIRC, Godel and Lob used the "|- Prov(...)" (or Bew(...)) predicate to essentially make them the same.
† The knowing is external to the system at hand, and the proving is internal to the system at hand. I go into detail about this in my blog posts linked above.
So I'm not sure it only applies to some special cases, I think several relevant incomputable problems might have this characteristic.
[1] https://en.wikipedia.org/wiki/Busy_beaver#Non-computability