3 ms·
Agreed that there are more powerful systems to verify this code, but these quickly face diminishing returns relative to their costs. On the other hand, collect
by Gankro 10y ago
Agreed that there are more powerful systems to verify this code, but these quickly face diminishing returns relative to their costs.
On the other hand, collections are embarassingly testable. It's never been clear to me that formal methods gain much over thorough fuzzing/unit testing in this context.
(rust's testing falls a fair bit short of thorough unfortunately and there have been a handful of mem safety errors in their impls. although I'm not aware of this ever leading to an exploit in an application. mostly caught quite early with the release trains as a buffer)
- vvanders 10y agoYeah, was going to say something similar. You shouldn't be reimplementing linked list unless you have a very good reason and if so you should be taking a careful look at what you do. Rust does a great job of error checking in the 99% case and the 1% of unsafe should be from well vetted libs. No different than trusting the kernel to do the right thing.
- jerf 10y agohttp://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://envisage-project.eu/proving-android-java-and-python-s... https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html https://research.googleblog.com/2006/06/extra-extra-read-all... Yes, you can asymptotically approach correct with testing, but it turns out that surprises can lurk for quite a long time if that's your approach. Of course, that's how most collections code works and what most of the world is built on, so yes, it is generally "good enough", but it is still worth pointing out that it is not necessarily correct, even after being out in the field for decades.
- Gankro 10y agoThis is, to some extent, moving the goal posts. You're considering "total correctness" whereas the focus of this stuff is largely "only" memory-safety.
- jerf 10y agoI would have been moving the goal posts if I didn't acknowledge that you generally get "good enough" code from what we're doing now. The point is that even being embarrassingly testable isn't a total panacea, though.
- kybernetikos 10y agoProving something correct is not a pancea either, although it can result in code that is generally "good enough". https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html https://research.googleblog.com/2006/06/extra-extra-read-all... > I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug.