Comment by roblabla
11 days ago
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.
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...
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.
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).
so why put them in before knowing if they work reliably? That's the YOLO part, to me
3 replies →
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
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.
2 replies →