While, yes, computability and provability are very closely related, it's important to get attribution correct.
More details on what Gödel's Incompleteness Theorem really said are in a sibling comment so I won't repeat them here.
Really? Says who?
Or perhaps you'll prove it from first principles. Although if turns out to be difficult, that's okay. Somebody mentioned something about systems being either complete or consistent but never both. Some things can be true but not proveably so. Can't quite remember who it was though.
[I believe that] it's important to get attribution correct.
- Futurama (kind of)
Gödel really was a rather unique mind, and the story of his death is kind of sad.. but I wonder if it takes such a severe kind of paranoia to look for how math can break itself, especially during that time when all the greatest mathematicians were in pursuit of formalizing a complete and consistent mathematics.
Godel means that we can't have an algorithmic box that we put a program into and out comes a true/false statement of halting.
Nothing is stopping you from writing the proof manually for each program that you want to prove properties for.
ALSO, you can write sub-turing complete programs. Those are allowed to have automated halting proofs (see idris et al).