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.)
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:
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.)