I can't see why being able to statically analyze the code brings it any closer to correctness - all it says is that you got your types right. In fact, switching to a lower-level language (as in "more detached from the problem you are trying to solve" such as C or C++) seriously harms your ability to even produce correct code.

Anyone who has chased a time-sensitive bug caused by data structures that mutate unexpectedly (be it by conflicting threads, be it by hardware changing it) can tell you that getting the types right won't help you a bit with making code that runs correctly on multi-core machines.