Ferrocene: Rust toolchain to safety-critical environments
ferrous-systems.com
ferrous-systems.com
https://rustacean-station.org/episode/067-quentin-ochem-flor...
Having AdaCore as a collaborator gives me great hope that Ferrocene will succeed and raise the bar for Rust standardization and language maturity.
There are huge swathes of MISRA which forbid things which not only aren't possible in Rust or SPARK, they'd probably make a lot of real world C programmers shake their heads in disbelief too. For example MISRA tells you not to put switch labels within blocks started by another switch label. Most C programmers probably had no idea they could do that, which is fine because they shouldn't. In experiments these MISRA rules don't trigger - nobody is actually writing the sort of C that's forbidden.
There are also a bunch of MISRA rules which just seem like style preferences, in experiments these don't seem to contribute to improved software correctness, the "bugs" identified by these rules don't interfere with correct program behaviour. Enforcement of such rules tends to breed resentment from programmers.
MISRA isn't useless, but that's actually an indictment of our industry. This very low bar is still tougher than a lot of code people are actually using. It's like you find out that your country's fire regulations only require a nightclub with 500 drunk people inside to have one working fire exit... and then discovering most clubs in the country don't meet this inadequate standard anyway.
I can't vouch for its accuracy, but https://github.com/PolySync/misra-rust seems to very much agree with you.
this specification is written based on the current behavior of rustc. The page even says that the specification will be updated as rustc is updated:
> If there is a mismatch between what the FLS says and how the compiler behaves, the specification will be updated.
So, rustc is not written to this specification, but rather this specification is written to match rustc.
So if I am writing my own compiler, using this specification, do I have to worry about the specification changing, if suddenly a regression is introduced to rustc, and the specification is updated to cover the regression?
mostly I don't understand. I'm sure someone could explain this and it will make sense to me.
It's basically an old version of the Rust Reference written out in a more bureaucratic manner.
(I see a little new material, such as the Name Resolution subsection, but even that is incomplete and I think wrong.)
Neither of these things is anywhere near close enough to being complete and correct to implement a compiler against.
If some old IE version did things a certain way, even the most modern browser will want to do things in a similar way to remain compatible. Therefore, the standards bodies will try to reverse-engineer the existing behaviors and then create standards based on those. That way, modern code can simply follow the spec and remain compatible.
The HTML5 parsing algorithm is an example of this. Old browsers tried to "fix" broken HTML by guessing where things like missing closing tags were supposed to go. The HTML 4 specification never described this logic, yet it was there in the wild. The new HTML 5 specification made a point of reverse-engineering the repair algorithms and actually documenting them, so now everyone can be compatible going forward, both with each other and with legacy. Just follow the spec.
An analogy from the C++ world: In late 2016, there was an evolving C++17 specification, and the latest versions of gcc and clang were starting to implement C++17 behaviors. But you could read the C++14 specification to understand "this is what everyone agreed on in 2014", and invoke your compiler with the -std=c++14 flag to get that behavior. If you already had older software written against the C++11 spec, invoke your compiler with -std=c++11.
Doesn't the reference implementation of the compiler already qualify as such a specification?
But the compiler mixes together spec-relevant details with implementation details (what bits go where). A written formal spec would only have the spec-relevant details.
I suppose a reference compiler needs only be functionally correct, not fast.
especially given that many use cases for this sort of thing are either embedded or close enough, and that Rust really relies on optimizations to produce good code, you need more than a bare minimum "it works" compiler to make the whole thing go.
My team's embedded project sets opt-level 1 even in debug builds, as no optimizations makes things impossible, flash size wise, and we're not even working with particularly small MCUs.
> Translation validation can be used even with a compiler that sometimes generates incorrect code, as long as this incorrect does not manifest itself for a given program. Depending on the input program the translation validation can fail (because the generated code is wrong or the translation validation technique is too weak to show correctness). However, if translation validation succeeds, then the compiled program is guaranteed to be correct for all inputs.
I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking. So you'd "freeze" the reference compiler and the equivalence checker (which would be qualified), and pair that with an upstream compiler with sophisticated optimizations. So long as the equivalence checker keeps passing, you're golden.
This is what CompCert does (or at least did when I last looked inside CompCert) for register allocation; the graph colouring algorithm is unverified, but a verified validator is used to check the colouring is correct.
Whilst this is relatively straightforward for something like graph colouring, it is substantially more difficult for comparing the outputs of two different compilers, which I think is what you are suggesting here?
There was some work to do a translation validation for the entire RTL -> LTL pass of CompCert, but I'm not sure how much progress was made or if this is currently used.
E.g. it's a huge amount of work to exhaustively formally specify the Rust type system (as opposed to just specify it in English). However, if you already have an assumed correct, but slow, type checker then your verification effort can boil down to just "does my compiler have a type error if [and only if if you care about more than just safety properties] the reference compiler has a type error?" That's still an enormous amount of work to verify, but is comparatively trivial to specify.
1. Say what you expect an implementation to do (the spec)
2. Check that the tool does what you say in step 1 (the implementation)
Part 2 on its own is not enough. The reference implementation is an implementation, but you still need an explicitly different reference to check said implementation against.
That it's a reference implementation means it's an appropriate thing to derive 1 from, which is of course what's happening here.
And rustc's massive test suite is very, very helpful in demonstrating 2.
1. Method resolution
2. Unstable?
In particular is it going to define lang items?
3. DST's
Rust has strange things like:
```
let a:&str = "str";
let b:&str = &"str";
```
Which is valid since str is a DST. Although slices and dyn trait are DST they have more strict rules there.
4. Qualified paths
There are more subtle things like qualified paths such as this testcase which could be argued is valid https://github.com/rust-lang/rust/blob/master/src/test/ui/qu... but there was some discussion on zulip which clarifies it: https://rust-lang.zulipchat.com/#narrow/stream/122651-genera...
5. Never type
TLDR: Overall I think its important at some point to start isolating what is the language outside of what version of libcore your running.
> 6.12:3 A method call expression is subject to method resolution
with "method resolution" marked as being a missing link.
This has nothing to do with DST but with type coercion.
The type of `b` is `&&str` but you requested the type to be `&str` which is fine as the compiler can coerce from `&&str` to `&str` in this case.
In the same way you can write
let b: &i32 = &&&&1;