What we're ultimately talking about here is compile time vs runtime.
Compile time errors, if you think about it, ultimately amount to the compiler being able to determine what problems you have in your program before it even gets run. It's obviously not an "arbitrary language" compiler, but I'll get back to that shortly. The compiler, in all its infinite wisdom, doesn't however list every problem which can be determined by the compiler. This is partially dependent on how well the compiler is written, but the primary reason for this is that a good many things are determined at runtime.
Runtime errors, as you are well familiar with I'm sure as am I, is any type of error which happens during execution of the program itself. This includes dividing by zero, null pointer exceptions, hardware issues, and many other factors.
The nature of runtime errors means you cannot anticipate said errors at compile time. If you could, they would almost be certainly checked at compile time. If you could guarantee a number is zero at compile time, then you could perform certain logical conclusions, such as dividing any number by that number will result in a arithmetic error caused by dividing by zero.
As such, in a very real way, the enemy of programmatically guaranteeing proper functioning of a program is performing runtime checks as opposed to compile time checks. An example of this might be performing a dynamic cast to another type. If this is allowed, you, the programmer, are essentially overriding the compiler's ability to know if that's a safe thing to do. Some programming languages have decided that this is acceptable while others will at least warn you at compile time.
Another good example might be allowing nulls to be part of the language, since null pointer exceptions could happen if you allow nulls. Some languages have eliminated this problem entirely by preventing variables not explicitly declared to be able to hold null values to be declared without immediately being assigned a value (take Kotlin for example). While you cannot eliminate a null pointer exception runtime error, you can prevent it from happening by removing the dynamic nature of the language. In Kotlin, you can force the possibility of holding null values of course, but it goes without saying that this is a metaphorical "buyers beware" as you have to explicitly state it as such.
Could you conceptually have a compiler which could check errors in every language? Yes, but it would likely be a clunky and highly unstable compiler in which you would have to necessarily provide the language being compiled beforehand. It also couldn't know many things about your program, anymore than compilers for specific languages know certain things about it, such as the halting problem as you mentioned. As it turns out, a good many pieces of information that might be interesting to learn about a program are impossible to glean. This has been proven, so it isn't likely to change anytime soon.
Returning to your primary point. Methods are not automatically thread safe. There is a practical reason for this, which is that thread safe methods are also slower even when threads are not being used. Rust decides that they can eliminate runtime problems by making methods thread safe by default, and that is their choice. It comes at a cost though.
It may be possible to mathematically prove the correctness of a program, but it would be with the caveat that you would have literally zero runtime features in the language. You would be able to read this language and know what it does without any surprises. The language would probably look very mathematical in nature, and that is likely no coincidence there. The second caveat is that runtime errors still happen, which may have nothing to do with the program itself. Therefore, the program can be proven correct, assuming a series of assumptions about the computer it is being run on are accurate and don't change, which of course always does happen anyway and often.