Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru...
by kybernetikos on Monday July 11, 2016 @03:05AM
(#12069336)
Proving 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...
> 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.
Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru...
by Gankro on Monday July 11, 2016 @12:12AM
(#12068842)
This is, to some extent, moving the goal posts. You're considering "total correctness" whereas the focus of this stuff is largely "only" memory-safety.
Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru...
by jerf on Monday July 11, 2016 @08:59AM
(#12070706)
I 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.
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.