Programs absolutely can be proven to be correct. Lousy programs are hard to prove. To do it even reasonably well, you have to evolve the program and proof hand-in-hand.
You can't automate the proof because of the halting problem. You can, however, manually prove the post-conditions and preconditions of any arbitrary statement, or sequence of statements.
You must read Dijsktra's A Discipline of Programming.
Then, you must read Gries' The Science of Programming.
Then you'll know how to prove programs correct.