Hacker News new | past | comments | ask | show | jobs | submit login

That was a very in-depth reply and is very appreciated. One point I did not expect that core and alloc are not qualified yet. In any case, you motivated me to do some research of my own to fill in the gaps in my own understanding. What follows is my attepmt to summarize all of this in the hope that you and anyone else reading it may also find it helpful.

I want to take a step back: why does the automative industry care about certain qualifications? Because the legaslative mandates that they follow them so that cars are "safe". In Germany the industry is required to follow whatever the "state of the art" is. This is not necessarily ISO 26262, but it might be. It might also be one of the many DIN norms, or even a combination thereof.

ISO 26262 concerns itself with mitigating risks and hazards introduced by safety-critical systems and poses a list of technical and non-technical requirements that need to be fulfilled. These concern both the final binaries and to some degree the development process. As you pointed out, the manufacturer needs to ultimately prove to some body that their binaries adhere to the standard. Use of a qualified compiler does not appear to be strictly necessary to achieve that. However, proving properties of a binary that is the result of a compilation process, is prohibitively difficult. We'd rather prove properties of our source code.

However, proving properties of source code is only sufficient to show properties of the binary if the compilation process does not change the behavior of the program. This is where having a qualified compiler seems to come in. If my compiler is qualified, I may assume that it is sufficiently free of faults. Personally, I'd rather have a formally verified compiler, but that's obviously a much larger undertaking. (For C, CompCert [0] exists.)

Now, as you point out, none of this helps if my own code is bad. I still need to certify my own code and Ferrocene can be a part of that. However, to circle back to my prior question of additional boxes that need to be checked: Yes, any Rust code written (and any parts of core, alloc, and std that are used) needs to be certified, but Ferrocene's rustc is ready to be used in software aiming for ISO26262 compliance today. No additional boxes pertaining to rustc need checking; although, qualified core and alloc would certainly be helpful.

[0] https://www.absint.com/compcert/




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: