Re:Haskell and Rust
by pron on Sunday November 10, 2019 @10:59AM
(#21498454)
> I'd classify this error as functional correctness
It isn't. Functional correctness is about ensuring that the code matches the spec. Preventing those kind of bugs could have a positive or a negative impact on functional correctness, but they are not, in themselves, functional bugs.
> Such class of error is simply not possible in Rust's type system.
This doesn't have much to do with correctness, though, and it's is a common mistake when discussing correctness (a subject I have written extensively about https://pron.github.io/). I am not saying that eliminating a certain class of bugs is bad; it might actually be good (although it might also be bad), but it's far from simple. It is absolutely not the case that if one language eliminates a certain class of bugs and another one doesn't, then the first leads to more correct programs. This implication is just wrong, both in its internal logic as well as empirically. To get some intuition for why it's wrong, consider that when naively writing a program on paper, you introduce 100 bugs. When you actually program it, you must use a variety of methods, including tests to get rid of them. Now, if you use a language that eliminates 10 of them with its type system, it does not mean that given the same amount of effort, you'll catch more bugs in that language than the other. It's possible (indeed, we know it happens when we work with more powerful type systems like dependent types) that it's harder to write the program in the first language, and in the time it took you to eliminate those 10 bugs -- i.e. getting the program to compile -- you'll have found 20 in the other language. And it's certainly possible that overall there just wouldn't be much difference.
Again, I am not saying eliminating certain classes of bugs is bad. I am saying that it is absolutely not true that doing so is a certain path to better correctness.
In any event, Rust's type system does not directly increase functional correctness. It does eliminate some bugs that could cause functional correctness issues, but whether the approach's cost/benefit is significantly better or significantly worse than, say, Java or Python is very, very far from clear.
It isn't. Functional correctness is about ensuring that the code matches the spec. Preventing those kind of bugs could have a positive or a negative impact on functional correctness, but they are not, in themselves, functional bugs.
> Such class of error is simply not possible in Rust's type system.
This doesn't have much to do with correctness, though, and it's is a common mistake when discussing correctness (a subject I have written extensively about https://pron.github.io/). I am not saying that eliminating a certain class of bugs is bad; it might actually be good (although it might also be bad), but it's far from simple. It is absolutely not the case that if one language eliminates a certain class of bugs and another one doesn't, then the first leads to more correct programs. This implication is just wrong, both in its internal logic as well as empirically. To get some intuition for why it's wrong, consider that when naively writing a program on paper, you introduce 100 bugs. When you actually program it, you must use a variety of methods, including tests to get rid of them. Now, if you use a language that eliminates 10 of them with its type system, it does not mean that given the same amount of effort, you'll catch more bugs in that language than the other. It's possible (indeed, we know it happens when we work with more powerful type systems like dependent types) that it's harder to write the program in the first language, and in the time it took you to eliminate those 10 bugs -- i.e. getting the program to compile -- you'll have found 20 in the other language. And it's certainly possible that overall there just wouldn't be much difference.
Again, I am not saying eliminating certain classes of bugs is bad. I am saying that it is absolutely not true that doing so is a certain path to better correctness.
In any event, Rust's type system does not directly increase functional correctness. It does eliminate some bugs that could cause functional correctness issues, but whether the approach's cost/benefit is significantly better or significantly worse than, say, Java or Python is very, very far from clear.