3 ms·
The type system of Rust does so much more than just ensure "undefined-behavior-safety" and increased type safety of any language often does wonders to improve f
by Too 7y ago
The type system of Rust does so much more than just ensure "undefined-behavior-safety" and increased type safety of any language often does wonders to improve functional correctness.
If i had a penny for every time someone forgot to check the return code or errno in a C program i would be a millionaire by now. Such class of error is simply not possible in Rust's type system. I'd classify this error as functional correctness, it has absolutely nothing to do with undefined behavior or anything like that, hence Rust does improve functional correctness.
Other common error i see i C# for example is that because of the GC everybody just passes objects around wildly without thinking of ownership, eventually there is a reference to some object everywhere, often in multiple threads, and you have no idea who is the real owner and who is just borrowing. Every reference is mutable so it is often very difficult to understand who is mutating it. Rust's immutability by default with only one mutating reference allowed at a time, would prevent this class of error also. (This isn't necessarily an error in itself but usually this spaghetti eventually leads to functional errors)
I do see your point though and agree that it would be very interesting to see a statistical evidence of how well this translates to productivity and end user perceived functional correctness. It could for example be that all such errors are weeded out during testing anyway, which leads us down the endless rabbit hole debate of dynamic vs static programming language. Though in my experience the closer to compilation you can find an error the better. Especially in larger teams where types not only help yourself but also describe the intent of the code for others.
- pron 7y ago> 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/ 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.