The Rust compiler had some severe bugs in the past which undermined the effectiveness of the memory safety. There is the saying in software engineering that the number of undiscovered errors in the system is proportional to the number of discovered errors. On the other hand Ada compilers used to be subjected to strict validation procedures in the past, and the AdaCore toolchain has an ISO 26262 and IEC 61508 qualification. That was the source of my remark.
back
2 comments
> There is the saying in software engineering that the number of undiscovered errors in the system is proportional to the number of discovered errors.
I think that's true for software developed under similar processes, but (for instance) if you're comparing software that has unit tests and software that doesn't, the constants are probably wildly different. Your tests (or even the process of thinking about writing testable code) will discover a number of errors but will hopefully drive the number of actual errors down.
To be clear, I'm not making a statement on whether Rust or Ada is better-tested or better-developed, but I will note that Rust goes out of its way
I'm also curious about these bugs - I'm aware of bugs in the standard library (which is developed in the same repo as the compiler), but they only undermine memory safety against hostile source code, and hostile source code has lots of other options (unsafe, /proc/self/mem, ptrace, ...), i.e., the Rust compiler is not a sandbox. I'm not aware of severe bugs in the compiler, and I'm not aware of standard library bugs against hostile user input by well-intentioned source code - e.g., there shouldn't be things like the 2001 sudo "vudo" exploit.
> I think that's true for software developed under similar processes
Of course, this is not a law of nature, but simply a reasonably plausible heuristic, which somewhat justifies my reluctance to a new technology, which was received with much enthusiasm.
Ok, but a formally verified compiler is a very different beast from a high quality compiler. We can realistically hope the Rust compiler team significantly improve the correctness of the compiler, but full formal verification is unlikely.
CompCert is an extremely impressive achievement, and compiles a near-complete subset of standard C. A verified Rust compiler would be an enormous undertaking, and would need a very skilled team. It also wouldn't be worth trying unless the Rust language were very stable, which, if I understand correctly, it isn't.