Ask HN: What does a formal memory model entail?

I asked this question in a thread recently but I was too late in posting to receive a reply. The article being discussed mentioned offhandedly that rust has no formally defined memory model.

What does it mean for a language to have a formally defined memory model? What benefits does having one confer? Is it hard to specify one? Why?