alt Hacker Newsso what I take from this is that the rust compiler does not guarantee the stuff it claims to. Because new features of the type system is just being yolod instead of formally proven
EDIT: I said new features of the type system and more importantly, their interactions with the ever growing list of other features, not new features in the compiler. Totally different things. The compiler could be perfectly implementing the wrong choice of algorithms in the first place.
Replies
No mainstream compiler is formally proven. If you want a verified compiler, you pretty much have to choose between using a subset of standardml or a subset of C and the one proven compiler for each.
There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.
The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.
As you can see, this is a true statement, but HN really really really hates it for some reason.
Yes. When people describe Rust as "a memory-safe programming language" they are describing an aspirational vision, and not a programming language that has actually been designed with sufficient rigor to guarantee memory safety. Any failure of rustc to actually guarantee this is just a bug in rustc itself, a failure to properly implement the Rust spec, because the closest thing Rust has to a spec is literally just the vague ideal that the compiler should guarantee safety somehow.
Rust cannot fail, it can only be failed.
There never was formal verification of the entire rust compiler, or even its complete borrow checker/type system. There has been verifications on _subsets_ of them.
Also, a lot of those soundness issues aren't related to new features _at all_, but usually due to poor assumptions made in optimizations.
The soundness bugs _are_ taken seriously though, and are slowly being patched out. A lot of the links in OP are now closed because Rust either changed how it generates code to avoid the issues, or fixed LLVM.