The undecidability of the Halting Problem implies that there exist Turing Machines such that you can't prove whether they halt or not in whatever logical system you're using (let's say ZFC)$^1$.
Have we found any such machines, and proven their halting's independence of ZFC?
It's easy to come up with problem specifications for which no proof could be found either way, but I'm looking for concrete programs you could write in any programming language. Put another way, I'm looking for a constructive proof of the Halting Problem.
$^1$ Proof: Consider a program H which takes a number N, enumerates all statements in ZFC searching for a proof that the Nth Turing Machine halts or does not halt. If every TM has such a proof, then H will eventually find an answer, and thus will solve the halting problem (unless there's a contradiction in ZFC, in which case the proof of halting for any machine can be found trivially).
Whether the halting of a particular Turing machine is provable (or disprovable) depends on which axioms you would accept a proof starting from, of course.
However, Gödel's Incompleteness Theorem shows how to construct, for every "reasonable" theory (that is, set of axioms) $T$, a particular logical formula $G$ where it is not provable from $T$ whether $G$ itself has a proof from $T$.
Thus, once you've chosen your theory $T$ (which could be for example Peano Arithmetic or ZFC set theory) construct a Turing machine $M$ which iterates through all possible strings of symbols and checks whether each of them is a valid proof of $G$. If it finds a valid proof it halts; otherwise it keeps searching.
Since $T$ cannot tell us whether $G$ has a proof, it cannot tell us whether $M$ will halt either.
The Gödel sentence itself is rather long and complicated if we want to write it out completely -- but fortunately we don't need to do that here: We can just program $M$ such that it starts by computing $G$ according to Gödel's instructions, and then begins looking for proofs. Writing an algorithm that will output $G$ is much more tractable than writing down $G$ itself. So if you want to see $M$ explicitly, a competent CS graduate student would probably be able to write it down in at most a few thousand lines of Scheme or Haskell.
Shorter solution: If we strip away the parts of Gödel's construction that are not immediately relevant here, we get this machine:
If ZFC proves that the machine doesn't halt, then it will halt (so ZFC can't be true). On the other hand if ZFC proves that it does halt, then (assuming ZFC is true) it will halt, which must be because it eventually finds a proof that it doesn't halt, so ZFC is inconsistent.