[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.