Until you guys write an actual formal specification, the compiler is the language.
The project is adopting Ferrocene for the spec.
Yes, the soundness hole itself is low impact and doesn't need to be prioritized but it undermines the binary "Zig is definitively not memory-safe, while safe Rust, is, by definition, memory-safe" argument that was made in response to me. Now you're dealing with qualitative / quantitative questions of practical impact, in which my original statement holds: "Zig is less memory safe than Rust, but more than C/C++. Neither Zig nor Rust is fundamentally memory safe."
You can of course declare that Safe Rust is by definition memory safe, but that doesn't make it any more true than declaring that Rust solves the halting problem or that it proves P=NP. RustBelt is proven sound. Rust by contrast, as being documented by Ferrocene, is currently fundamentally unsound (though you won't hit the soundness issues in practice).
- If a safe Rust program exhibits a memory safety problem, it is a bug in the Rust compiler that is to be fixed - If a Zig program exhibits a memory safety problem, it is a bug in the Zig program that needs to be fixed, not in the compiler
Wouldn't you agree?
> Ferrocene is intended to document the behavior of the current version of the rustc compiler, so it's just an effort to formalize "the compiler is the language".
I must admit I haven't read the specification, but I doubt they attempt to be "bug for bug" compatible in the sense that the spec enumerates memory safety bugs present in the Rust compiler. But am I then mistaken?
As to the Ferrocene specification, it explicitly states "Any difference between the FLS and the behavior of the Rust compiler is considered an error on our part and the FLS will be updated accordingly."
Proposals to fix the soundness hole in Rust either change the variance rules themselves, or require where clauses in certain places. Either of these changes would require corresponding changes to chapter 4 of the Ferrocene specification.
Right, this is from before it's adopted as the actual spec, because it was from outside the project, and so could not be.
Also, these goalposts are moving: it was "Rust doesn't have a spec" and now it's "I don't like the spec."
Fixing this soundness hole does not require a breaking change to the language. It is an implementation bug, not a problem with the language as specified. But even if it were, Rust's policies around soundness do allow for this, and the project has done it in the past.
If there is a proposed fix to the soundness hole that wouldn't reject some existing sound Rust code, please link to it; none of the proposed fixes I've seen do so. And yes, Rust's policies do allow for breaking changes in pursuit of soundness - likely some day many years from now safe Rust will indeed be sound and guaranteed to be memory safe.
I really don’t see how you can claim with a straight face that the two approaches are the same.
Look, I'm not saying the Zig and Rust approaches are the same. I explicitly stated that Rust is more memory safe than Zig (which is in turn more memory safe than C/C++).
This is because Rust has clearly delineated a "safe" subset of Rust which you have to explicitly opt out of that is mostly sound (and has a goal of eventually being entirely sound), has a culture of encouraging the use of the safe subset, and has taken a good approach to the interfacing of safe and unsafe code (i.e. if unsafe code is properly written and satisfies the exposed contract - despite the compiler being unable to verify this - then safe code can safely be linked with it).
All of this results in extremely low risk of memory corruption for Rust programs in practice (far lower than any other commonly used non-GC language with the sole exception of SPARK).
What you can't do though is reject the notion of memory safety being a sliding scale and draw a binary distinction between languages that are 100% perfectly memory safe and languages that are memory unsafe. Well you can, but Rust will fall on the side of memory unsafe for many years to come.
That is the absolute best description of memory safety I’ve heard expressed.