In 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.)