3 ms·
To be fair though, almost every language is unsound in that metric. In fact, only an implementation that is verified and translated from a formal specification
by lifthrasiir 3y ago
To be fair though, almost every language is unsound in that metric. In fact, only an implementation that is verified and translated from a formal specification with the verifier and translator also similarly verified (ad infinitum) would be sound. Even PL researchers are not that strict---many academic papers don't actually prove the whole soundness, because the proof process is more or less automatic for the vast majority of cases to who know enough PL theories. (I can't say it's "mechanical", since the reasoning is still required. But the reasoning itself is not too involved for intended audiences.)
Just like that not every security vulnerability is equally fatal, not every soundness bug is equally fatal. I reckon about three levels of severity: inherent to the design itself, not inherent to the design but reasonably user-visible, and pathological. As pcwalton pointed out, miri does show that this particular soundness bug is NOT inherent to the language design, and I believe that's true for most of 84 unsound bugs (please let me know any counter-example though, I haven't fully checked them). It remains to be seen whether there exist soundness bugs that are still user-visible enough.
- jart 3y agoBut languages like C / C++ don't claim to be safe.
- lifthrasiir 3y agoEven Rust doesn't claim to be "safe" without a qualifier. From the website: > Rust’s rich type system and ownership model guarantee memory-safety and thread-safety — enabling you to eliminate many classes of bugs at compile-time. Note that it explicitly mentions "memory" safety and "thread" safety, which has a specific but reasonable definition in Rust (for example, memory safety doesn't cover physical memory leak). Also it explicitly mentions which portion of Rust is responsible for such guarantees, namely "type system" and "ownership model", and it is reasonably claimed that the ideal implementation of both will indeed completely achieve such guarantees. To be clear, the current implementation is also very close to that ideal to make such claim meaningful, but there is always a difference between the ideal and the practice.
- jart 3y agoThen they should say "we're researching how to create a memory safe language" or "we've built a memory-safer language" rather than saying what they're saying.
- lifthrasiir 3y agoIf you like a pedantry, yeah. But it helps to know that almost everyone else don't like that pedantry.
- deleted 3y ago[deleted]
- mwcampbell 3y agoI agree with jart on this. Rust has gained a reputation for overzealous marketing (also called evangelism), and we who like and use Rust should do everything possible to reverse that reputation, by being honest, even to a fault, about known limitations.
- lifthrasiir 3y agoDon't get me wrong, I too agree on your sentiment (even though technically it wasn't a Rust's own fault), but I also believe that jart's claim was something else and a comparison with academic paper should be sufficient to show that.
- Georgelemental 3y agoBy that standard, no general-use programming language (even eg Python or Java) could ever be called "memory-safe". That level of pedantry is occasionally necessary, but not usually useful. In practice, I'd confidently wager the vast majority of Rust programmers have never encountered a soundness bug in the core language when not specifically hunting for one (I certainly haven't).
- jart 3y ago