The distinction of course is that the compiler checks what it is telling the programmer it checks, which is that both operands to + are of compatible types where a + operation is defined. The compiler is making no other contract. Whereas, the borrow checking is a contract about the inability to alias, yet the borrowck is not enforcing that when the programmer escapes to using raw pointers. The programmer of the raw pointer implementation is assured the borrowck won't allow his interface to be aliased, but the user of that checked interface has to presume that the programmer of the implementation is compliant behind that interface which employs the raw pointer. But that isn't even my main point, which is moreover that we are forcing the borrowck everywhere in a total ordering tsuris for the user, but then needing to escape out of it, and not only encapsulated in a tree of checked disjointness but also in cases where the borrowck will somehow have to be entirely subverted I guess by putting raw pointers in userland code (see my quote of myself below).
And when Circle / Square inherits from Ellipse / Rectangle in an OOP language, the subclassing paradigm is not lying about the fact that the invariants of Circle / Square are violated by the invariants of Ellipse / Rectangle in the mutable case (the error doesn't exist in immutable case).
I don't think there is one language that can satisfy everyone's preferences. For example, programmers will have different preferences on the mix of FP, imperative, immutability, low-level control, and high-level reasoning. I did mention a set of features that I think would be popular in a language, that currently don't exist as a complete set in any one language (although Haskelll and Scala get close but with idiosyncrasies and issues that cause me to think they are not going to be popular).
My apprehension regarding Rust was mostly merely arguing that I posit that aiming for total orders is an anti-pattern adding a lot of tsuris for very little gain{1}, and that it creates a frequent case where it is saying it has checked the invariants but has in fact delegated the checking to the programmer via the escape hatch of raw pointers, and in other cases we can't even do certain algorithms except by putting raw pointers in userland code. I may be wrong about the relative gain and the relative tsuris. I will merely quote again my most relevant statements and leave it as an open question that has not been thoroughly quantified. The market will quantify it over time. I don't think we are omniscient enough to know with certainty, but again I offer the following quotes as my insight or intuition on the matter and they may well be wrong or too one-sided or ... please remember I am all thumbs up and ecstatic about Rust's typeclasses and Crates.
{1} To reiterate or re-summarize again, appears to me that mutability control is a high-level concern, and most performance comes from high-level reasoning (profiling the code). Low-level performance is rarely the 80/20. Again I may be wrong about those priorities and it may vary by programmer and use case. YMMV.
Edit: we have all these wonderful PL advances that reduce tsuris and increase high-level expression such as first-class functions, lambdas (closures), type classes, and stackless coroutines or generators. I would like to see all those in a popular language asap. I am tired of waiting. Jettison all that OOP noise that is an anti-pattern. I realized that wasn't the reason Graydon Hoare created Rust. I've been reading his blog. He created Rust because he believes in low-level safety and thought that could help to build a better browser. I criticized Typestate back in 2011 when I first read Rust was considering it because type systems should never be separated (two different type systems in the same language). Now I am dubious (almost criticizing but aware of my lack of omniscience) about total ordering, low-level safety checks, which are only open under a tree of disjointness thus incompatible with open expression of partial orders (that is a generative essence attribute that I posit will prove to be an anti-pattern, but I'm not 100% certain). It was also a small world when I read today that he had been working on Stellar's consensus algorithm after he left Rust which I also analyzed a few months ago and had criticized as it would end up centralized (not realizing he was part of its implementation). And I see Graydon and I have entirely dipolar politics (I eat a lot of meat, love sports, and I'm not apologizing for being a man). So I don't expect a very significant chance we will be working together in the future although he seems to be very knowledgeable. Enjoyed reading his blog today. He is extremely shy (he admitted in his blog he feels awkward in social gatherings), I can only find one photo of the man on the entire internet and he is looking at the ground. As you can probably tell, I am an extreme extrovert. I don't get offended by Paul Phillips' (Scala) brash style, at least he wasn't as arrogant to me as others in the FP realm (Graydon also lamented the FP community tendency to arrogance or too serious in his blog). Rust community has treated me very respectfully and you also have my respect. I will exit with admiration of your tolerance.