[Ar-Curunir]

This is nonsense. Just because some small parts of the code are must be annotated as unsafe doesn’t mean that we’re suddenly back to C land. in comparison, with C the entire codebase is basically wrapped in a big unsafe. That difference is important, because in Rust you can focus your auditing and formal verification efforts on just those small unsafe blocks, whereas with C everything requires that same attention.

Furthermore, Rust doesn’t turn off all checks in unsafe, only certain ones.

,

[uecker]

If you think correctness is only about memory safety, only then you can you can "focus your auditing and formal efforts on just those small unsafe blocks". And this is a core problem of Rust that people think they can do this.

[erik_seaberg]

Memory and concurrency safety need to be the first steps, because how can you analyze results when the computer might not have executed your code correctly as written?

[Ar-Curunir]

my comment (and indeed in this entire comment chain) is within the context of memory safety. This should have been clear because of the focus on unsafe, which, compared to normal Rust, relaxes only memory safety.

Obviously if you want to get formal guarantees beyond that property, you have to reason about safe code also.

(Also, the comparison in this entire chain is against C, and the latter is better than Rust in this regard… how?)

[uecker]

Yes, this discussion is about memory safety, but this does not invalidate my argument. There is no point in only auditing your code with respect to memory safety, so the argument that you can simply ignore everything outside "unsafe" blocks is simply wrong.

[Ar-Curunir]

You can’t expect to hop in the middle of an ongoing discussion, ignore the context of that discussion, and then hope to be taken seriously.