I think you'll find that if you want to prove a program correct (which vanishingly few people really do in practice, but anyway) you will find it infinitely easier to do so if the language it's written in is type- and memory-safe.
Even if you're talking about the looser notion of "does my program behave correctly", we have a lot of evidence that using simpler unsafe languages doesn't produce more correct programs than more complex safe languages. See: basically every piece of C code in the wild.
Even if you're talking about the looser notion of "does my program behave correctly", we have a lot of evidence that using simpler unsafe languages doesn't produce more correct programs than more complex safe languages. See: basically every piece of C code in the wild.