> How do you address the inherent unsafeness of hardware? Even "pure" functional languages are hacking around this...

By proving the hardware correct. Then if you're running proven memory safe Rust on formally verified hardware, you're guaranteed by construction that the Rust you're writing is memory safe (for the formally-specified notion of "correct" and "memory-safe" in use, which will probably issues like manufacturing problems and compiler bugs).

A Google search for [hardware formal verification] can get you started, if you're interested. There's been a good deal of work in this area.

Assuming you mean the weak memory models, the compiler normally enforces the guarantees made by the semantics of the programming language ... assuming you have a semantics.

That's where this project comes in and that is why the C++ memory model definition/formalization was so important. Programmers need to know what guarantees the compiler gives about the behavior of the code after compilation and the semantics is the final word.

I think the assumption is that the hardware spec is correctly implemented and that it runs ideally well. Otherwise that would require some kind of probabilistic model I guess. But you're right, "purity" is a simplification. Computations are inherently effectful(and even side-effectful depending on the reference frame) in practice.

Also, I seem to understand that the research is merely done in the context of the Rust language. The title is maybe a bit too much :)

Elaborate on what you mean please?

What do you mean? Do you mean that hardware is unreliable or might break and thus even a sound program, or a program that doesn't do anything that counts as unspecified behaviour, is not 100% safe? Or that with "unsafe" escape hatches often needed to directly interop with hardware are a problem?