The article says that Rust does not have a formally defined memory model. What is an example of a formally defined memory model?