Wrong, wrong, wrong. As I said, race conditions caused by non-exclusive mutable access (such as modifying a collection while iterating over it) are trivially prevented by forbidding non-exclusive mutable access! Which is what Rust does. Not all race conditions can be prevented, obviously. But that does not mean that none of them can. I'm not sure what you mean by "local, syntax-based analysis" given that type systems are neither local nor syntax-based. Do you perhaps have a failure of imagination of what sorts of invariants a powerful type system is able to enforce?

Do linear and/or dependent types change this statement?

You can always write nonsensical code like this (pseudocode):

   def counter = 0

   def increment() {
       def tempcounter = null
       counter.lock {
           tempcounter = counter
       }
       tempcounter++
       counter.lock {
           counter = tempcounter
       }
   }

Exclusive access to counter is guaranteed and therefore memory safety has been maintained but reads and writes may still be interleaved and cause incorrect results.

Your point is a good one: a correct program might still be wrong.

I think the argument is that it's inadequately typed. I.e. the program itself is correct because the semantics aren't captured properly.

If you had a type system that captured that tempcounter was derived from an earlier version of counter, then it could enforce that the assignment of counter in the second lock does not depend on a previous version of counter. Runtime enforcement would be trivial in most languages by making counter a monad that essentially carried a DAG around to detect this sort of problem. I'm pretty sure though that you could enforce this at compile time with dependent types in something like Idris.