Author here. I'm currently interning at Mozilla with the goal of writing the "advanced" companion to the TRPL (The Rust Programming Language book): TURPL (The Unsafe Rust Programming Language).
In the process I'll need to wrangle various members of the community -- particularly core team members -- to determine the things that we actually intend to guarantee in safe code, and what unsafe code is allowed to "do".
This post was intended to kick off that effort by:
* Making it clear that stuff is unclear
* Asserting my beliefs on what things should be
* Getting the whole internet mad at me so that they can explain what it should actually be
So, please, single file: Get Mad On The Internet At This Guy
I think the most important point you make is that unsafety confounds local reasoning, requiring reasoning about all the possible interactions a block of code might have with everything else. One of my favorite things about (safe) Rust (and functional languages in general) is exactly this local reasoning capability that you give up in unsafe code. It's still not clear to me whether or not it's harder to write correct-in-all-cases unsafe Rust code than correct-in-all-cases C/C++/etc. code in general.
As I was reading, I was thinking it would be nice for crates.io to include an indication of "level of unsafety" for each crate, but then you went and pointed out that the naive metrics for it would be dependent on stylistic choices. I wonder if you could transform to a "minimally unsafe representation", at either the code or AST level, and evaluate that.
Looking forward to TURPL, and especially interested in learning more about how unsafe code interacts with destructors, which seem particularly fraught.
In the process I'll need to wrangle various members of the community -- particularly core team members -- to determine the things that we actually intend to guarantee in safe code, and what unsafe code is allowed to "do".
This post was intended to kick off that effort by:
* Making it clear that stuff is unclear
* Asserting my beliefs on what things should be
* Getting the whole internet mad at me so that they can explain what it should actually be
So, please, single file: Get Mad On The Internet At This Guy