3 ms·
I think we'll just have to agree to disagree. I'm not certain you're wrong, so we'll have to see how it shakes out. And I love what the Zig project is doing, so
by burntsushi 4y ago
I think we'll just have to agree to disagree. I'm not certain you're wrong, so we'll have to see how it shakes out. And I love what the Zig project is doing, so I wouldn't at all be surprised if they find some other way here that works well in practice.
Otherwise, I do think you underestimate the differences between an annotation like 'unsafe' and what you can find easily only through a static analysis tool. The key bit of the 'unsafe' annotation is the concept of "safe API" that it inspires, and also gives one a vocabulary for talking about things like 'soundness.' For example, you can mark Rust functions as 'unsafe' and then document the preconditions for avoiding UB. If you didn't mark that function as 'unsafe', then we would call it unsound because there exists an input that could cause UB, but it does not necessarily result in UB for every input.
The annotation gives people a way to talk about and crystalize precisely what it means for an API to be safe for all uses. It funnels everything about memory safety down into that one concept and makes reasoning about it much much easier. Without an annotation like that, it's cumbersome or downright difficult to even talk or communicate about soundness.