Rust needs an official specification
Rust needs an official specification
Can we currently reason about Rust code with absolute certainty? Not really, but we should be able to. In this article, we dive into the reasons why it may be time for a Rust specification.
This article somehow links to both the Reference and the Ferrocene spec, but still concludes that an official non-Ferrocene spec is necessary.
Why doesn't the Ferrocene spec accomplish what the author wants? He states:
In other words, without a clear and authoritative specification, Rust cannot be used to achieve EAL5.
What? Why can't the Ferrocene spec (and compiler) be used? Do Ferrocene and TÜV SÜD not count as "some group of experts"?
(Regarding the author's opening paragraphs, the Reference does make the same distinction about drop scopes for variables versus temporaries, though I can see why he finds the Ferrocene spec clearer. But that doesn't demonstrate that the Reference is useless as a stand-in for a specification.)
It's not because we have tested this program extensively on every C++ compiler, but because the language rules of C++ say so.
Debatable. Saying things in a prose specification doesn't magically make them happen. Tests and reference models can though.
I also don't really agree with the SIL requirements that languages need to have rigorous specifications to be safe. Clearly it's better if they do, but would your rather fly on a rocket controlled by C code or Rust code?
IMO a specification would be really nice to have, but it main purpose is to tick a certification checkbox, which is why the only one that exists was written specifically for that purpose.
The specification does not make anything happen but it enables you to say "the implementation is wrong". Of course, you can say that without a spec as well but what does "wrong" mean then? It just means you personally disagree with its behavior. When "wrong" means "inconsistent with the spec" everybody involved can work with more clarity and fewer assumptions. Wrong assumptions can kill people flying rockets.
You can say the Rust implementation is wrong if it doesn't conform to the Reference. That is not the same as "you personally disagree with the behavior."
Rust's guarantees about the behavior of safe code are far stronger than anything C or C++ provides, with or without a formal spec.
you can say that without a spec as well but what does “wrong” mean then? It just means you personally disagree with its behavior.
Nope. Specs can have bugs. Here are the bugs in the C++ spec for example:
https://www.open-std.org/jtc1/sc22/wg21/docs/cwg_toc.html
As I said, specifications are useful and desirable, but the SIL's dogmatic "no spec = unsafe" is clearly not based in reality.
It's not as if nothing is being done on GitHub we have both: rust-lang/spec which is being folded into rust-lang/reference.
I'm not sure why we don't have an official spec, I assume that reference was originally for rustc in particular and might include some internal weirdness instead of being a proper spec. Kinda like how gcc has some internal magic that isn't strictly to C spec.
I guess what happened was: spec for rustc -> developed rustc -> ferrocene developed from rustc spec -> "we don't have a generic rust language spec"
There is indeed a caveat in the introduction to the Reference that there may be statements in it that are specific to
rustc. However, the authors strive to keep statements about the implementation separate from statements about the language.The main reason there's not yet an "official" spec is that creating one takes enormous time and money, which are always limited resources. (Note that both C and C++ had no formal standard for over a decade after their initial release.) The Reference is "good enough" to make a formal spec not strictly necessary, and the existence of Ferrocene makes it even less necessary, since anyone who absolutely needs a spec can use Ferrocene.
Most importantly it takes a lot of effort and is essentially outdated the moment it is done unless you slow down and complicated every other process by funneling every change through the spec first.
I'm actually surprised there is no specification. It's how I thought languages were written: spec first, implementation later. Do RFCs serve this purpose?
That's actually not how any language has ever been written, though it's easy to get that impression from how much the C and C++ communities emphasize their formal specifications.
But in fact, both languages were in production use for over a decade before they had a formal spec. And languages with formal specifications are actually a tiny minority of programming languages.
That requires a complete picture and all possible use cases from the start. Initially when a language is new and hardly used there are much to benefit from flexibility and trying new concepts. Then as the language matures, a more formal process is needed to ensure stability. There is a reason these discussions comes now, since rust is in a very stable phase.
There might also just not be a single spec because the information is spread out over RFCs instead of being collected in a central location.
Welcome to the real world. /s