The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it.

Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.