4 ms·
The point of the borrow checker is to replace the global property 'all memory has an owner' with the (approximate, conservative) equivalent 'all code passes the
by chriswarbo 6y ago
The point of the borrow checker is to replace the global property 'all memory has an owner' with the (approximate, conservative) equivalent 'all code passes the borrow checker'.
By tracing ownership information through each component, and forbidding (or ignoring via `unsafe`) situations which cannot be traced in this way, the latter property can be decomposed and solved locally.
In other languages, like C++, we may still want this global property, but we can't break it down into local reasoning. Even if we decide on an approximate, conservative equivalent like 'all code passes STATIC ANALYSER X', getting local reasoning to work would require enough changes that it's arguable whether we're actually programming in the same language anymore. For example, we may need to add extra annotations to our code (which aren't present in existing codebases); we may need to extract extra information from sources (preventing the normal use of separately-compiled libraries); we (and our dependencies!) may need to avoid certain valid/legal patterns of code which the analyser can't handle; etc.
Writing the above, I'm reminded of trying to use the mypy type checker in Python!
- Animats 6y agoIn other languages, like C++, we may still want this global property, but we can't break it down into local reasoning. That's exactly it. You want some set of machine-checkable constraints which add up to the desired global properties. Rust managed to do that. Attempts to fix this in C++ yield a set of slightly leaky constraints which sort of almost do that. Fixing this requires taking things out of the language, which is unpopular. It's embarrassing that the code below still compiles with default gcc options, in either C or C++ mode. Yes, it's terrible C++. The compiler allows it. #include <stdio.h> #include <string.h> int main(int argc, char* argv[]) { char buf[20] = "\0"; char* s = buf; for (int i = 0; i<argc; i++) { s = strcat(buf, argv[i]); } printf("%s\n",s); } (Even Microsoft has "strcat" deprecated by default.)