Hacker News new | ask | show | jobs
by uecker 180 days ago
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.
1 comments
aw1621107 180 days ago
> 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.

link
uecker 180 days ago
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.
link
aw1621107 179 days ago
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.

link