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 beca

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.