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.

▲

meltyness 2 hours ago | parent | next [-]

https://github.com/model-checking/verify-rust-std

hm, there's an effort but scoped only to the std

It's terrifically complex: https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty...

▲

vrighter 2 hours ago | parent | prev [-]

not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.

▲

afdbcreid an hour ago | parent | next [-]

The eventual goal is verification of the full system. Not the implementation, yes, that's infeasible. But this will mean all soundness bugs will be either found and fixed or we'll know how to fix them once they're found. In any way they won't be fundamental (which is believed to be the case today, but not proven).

▲

vrighter an hour ago | parent [-]

so why put them in before knowing if they work reliably? That's the YOLO part, to me

	▲	cscheid 9 minutes ago \| parent \| next [-]
		The same combination of reasons we've been doing these kinds of heuristic implementations forever: - people still get value off of an incomplete implementation, because we are allowed to be mindful of the issues (see, eg, UB in C++). In other words, many, many more bugs have been prevented by the borrow checker working as intended than have been caused by it working poorly. It's not particularly close. - theory almost always moves slower than practice The mutable state situation pointed out by the grandparent poster was a famous issue in typing SML under mutability that required serious changes in the language, see Section 4.2 here: https://smlfamily.github.io/history/SML-history.pdf These were Turing-award caliber people figuring it out and, according to your definition, "yolo"ed it. This stuff is _hard_, and these driveby comments truly aren't helpful.
	▲	dwattttt 9 minutes ago \| parent \| prev \| next [-]
		You're claiming that this bug that reproduces back to Rust 1.4 (2015) is a sign they're adding too many features to make sure they don't introduce bugs? Or do you have bugs that are due to these recent features?
	▲	vlovich123 6 minutes ago \| parent \| prev [-]
		Because there’s real value delivered even before that? Perfect bring the enemy of good and all that

▲

streetfighter64 2 hours ago | parent | prev [-]

It holds that ¬(∀subsets: isverified(subset)) but it's not true that ∀subsets: ¬isverified(subset), which it think most people would interpret "the whole system is unverified" as

	▲	vrighter an hour ago \| parent [-]
		If I independently verify that subsystem A properly consumes apples, and that subsystem B is properly emitting oranges, but never verify that subsystem A is receiving apples, and just connect subsystem B to it, then yeah, the system is not verified.