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.

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.

Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.

Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?

Important to note that this is is not a bug in the type system itself, it's a bug in the borrow checker not enforcing invariants that the type system says that it should, and formal verification of the type system would not have helped here.

The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.

The font color is so close to the background now that I can't even read your edit. Sorry, bud.

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.