Remix.run Logo
▲ afdbcreid an hour ago

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