rust-memory-model

Sorry for not responding sooner, but I agree with you completely that the right thing to do is not to focus on "how many" `unsafe` lines you have, but how well encapsulated they are into a module that can't be broken by outside input. And I'm glad we both see this. My "problem" is less that `unsafe` doesn't do the things I mentioned, but that whenever Rust and `unsafe` come-up there tends to be lots of people who don't understand what it is, or how it works, and I think that is a very dangerous mindset because it leads to completely pointless (and dangerous, from a safety perspective) stuff like how that paper literally measured how many lines were `unsafe` and displayed it as a percentage to prove their code was good. With all that said, while this is a separate topic, I think that the complete lack of a spec for lots of details surround

As far as I know Rust doesn't have a memory model fully defined yet, but their type system already helps a lot. https://github.com/nikomatsakis/rust-memory-model A bit old, https://blog.rust-lang.org/2015/04/10/Fearless-Concurrency.h...

There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/. One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model

It's not only a MIR issue, it's also an issue of how many optimizations should be allowed when you also need to be able to make some assumptions about your data in unsafe blocks. For example if you simply added the obvious attributes everywhere, interior mutability (Cell, RefCell, UnsafeCell) would most certainly break. The exact rules around unsafe rules are still being discussed (see https://github.com/nikomatsakis/rust-memory-model), so until that is done some of these optimizations are very unlikely to be implemented because they can make a lot of unsafe code illegal.

While hiding unsafe parts of code behind safe interface works great in Rust, especially that ownership / borrowing rules expresses much more than is possible in other mainstream languages (in Java you wouldn't know if you are the owner of collection returned collection, or maybe it just a view, etc.), there is one thing that I never seen addressed in this kind of arguments: Writing unsafe code in Rust is harder than doing it in C/C++, because Rust introduces a whole new class of undefined behaviours that is just absent from C/C++. See [0], [1] or [2] in general for examples. [0] http://smallcultfollowing.com/babysteps/blog/2017/02/01/unsa... [1] http://smallcultfollowing.com/babysteps/blog/2016/05/27/the-... [2] https://github.com/nikomatsakis/rust-memory-model