[uecker]

The first misunderstanding is that safety is a property of the language or not. Rust marketing convinced many people that this is so, but C can be safe or unsafe. Fil-C shows that even all of C can be memory safe (but at a substantial cost in performance). But even just with GCC and Clang, array access and signed integer can be made safe with a compiler flag, and a violation then traps and this is similar to a Rust panic. The cases which can not be dealt with easily are pointer arithmetic, unions, and free and concurrently related issues. And it is very well possible to isolate and review all of these. This will not find all bugs, but neither does this work perfectly for Rust "unsafe" as this bug (and many others) nicely illustrates.

[wmanley]

I guess that means you're using the colloquial meaning of the word safety/unsafe rather than the rust definition. It's worth being explicit about that (or choosing a different word) in these discussions to prevent confusion.

For Rust safety (meaning no UB) most definitely is a property of the language. If a module does not contain unsafe and the modules it uses that do contain unsafe are implemented soundly then there is no UB.

In C UB is a part of the language.

[uecker]

No, in the comment you reply to, I am using safe/unsafe in the Rust sense. E.g. signed overflow changed to trap avoids the UB.

Also "If .. are implemented soundly" sounds harmless but simply means there is no safety guarantee (in contrast to Fil-C or formally verified C, for example). It relies on best-effort manual review. (but even without "unsafe" use anywhere, there are various issues in Rust's type system which would still allow UB but I agree that this is not that critical)

In C UB is part of the ISO language specification, but not necessarily part of a specific implementation of ISO C. If you argue that the ISO spec matters so much, I like to point out that Rust does not even have one, so from this perspective it is completely UB.

[aw1621107]

> Also "If .. are implemented soundly" sounds harmless but simply means there is no safety guarantee (in contrast to Fil-C or formally verified C, for example).

Don't those also depend on implementations being sound? Fil-C has its own unsafe implementation, formal verification tools have their trusted kernels, it's turtles all the way down.

[uecker]

The implementation itself being sound, yes. And yes, in Rust if you only use sound libraries (in combination), never use unsafe yourself and ignore the known defects in Rust, then it is also guaranteed to be safe. But in system programming, you usually have to use "unsafe" in your own code, and then there is no guarantee and you make sure the could has no UB yourself, just like in C.

[aw1621107]

Sure. My point is mostly that the problem is less that your safety guarantees rely on correct implementations (since that applies to all "safe" systems as long as we're running on unsafe hardware) and more that the trusted codebase tends to be quite a bit larger for (current?) Rust compared to Fil-C/formal verification tools. There are efforts to improve the situation there, but it'll take time.

Does make me wonder how easy porting Fil-C to Rust/Zig/etc. would be. IIRC most of the work is done via LLVM pass(es?) and changes to frontends were relatively minor, so it might be an interesting alternative to MIRI/ASan.