Hacker News Reader

Only if the data structures aren't exposed to outside of the program, in which case, Rust cannot guarantee safety from data race problems caused by OS IPC mechanisms like memory mapped data, shared memory segments or DMA buffers, accessed by external events.

I would say it can go further than that: Rust enables you to construct many APIs in a way that can’t be misused. It’s not at all unique in this way, but compared with C or Go or the like, you can encode so many more constraints in types.

Minor nit: formal verification doesn't guarantee correctness.