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.