> [Rust is] not quite undecidable but it is still very much NP-hard.
> Languages like C, C++, or Ada ... make little to no attempt to enforce correctness
Both statements are laughably false, but for different reasons.
Both are based on the Doctrine of Rust Exceptionalism, which requires that Rust is not just a variation on a theme, but fundamentally different from other languages. Like most doctrines, this one is indefensible.
Rust compilation, like C++ and Haskell, is undecideable, not just NP-hard. Non-terminating compilation is artificially curtailed, thus failing to produce an open set of what would have been correct programs.
The Rust compiler performs certain correctness checks that other languages do not. It rejects an infinite set of correct programs that its correctness checks cannot resolve. In this as in all other particulars, Rust is very much on the continuum with other languages. All strongly-typed languages perform a huge variety of correctness checks, some built-in, others programmed, with great success, rejecting the large majority of incorrect programs people write. As a consequence, it is very common for Rust, C++, and Haskell programs to run correctly the first time, once the compiler is satisified.
I don't believe in any of that Rust exceptionalism BS. Rust is just a strongly typed language just like Haskell or any other strongly typed languages. This strong typing (particularly through the borrow checker) gives the Rust compiler the ability to verify properties about the code like any other strongly typed language. The mistake that Rust makes is that they attempt to make the verification a language requirement while nearly every other language either makes it optional or keeps the verification in a library or tool external to the standard.
With Rust though a significant part of the value in things like the borrow checker is that it has the assertion that if you break the rules set out by the "standard", the code doesn't compile. Even Haskell doesn't make the mistake of trying to enforce something like that (instead it's libraries that normally add that verification but those aren't part of the standard).
My point is that Rust has language requirements that force the language compilable by the compilers to never be close to or equally covering the entire language defined by the "standard".
There will be normal (and emphasis on normal) programs that will not be compilable in Rust on certain compilers but will work just fine on others due to the search space on the type solver or the borrow checker blowing up. These issues will also likely pop up in between versions of the same compiler when changes to the internal representation cause certain cases to fall outside the search space.
The only thing the Rust devs can actually do to solve this problem is to add arbitrary restrictions to the language spec based on the limitations of existing compilers.
This issue isn't unique to Rust but basically every other major language has gotten around the problem by not making it a problem in the first place.
---
This comes back to the point in my original comment. Rust the language based on the compiler will likely not be consistent within Rust the language based on the "spec" (whatever it ends up being). There will be normal code that fails to compile due to seemingly arbitrary changes triggering combinatorial explosions.
With C, C++, Haskell, etc this issue can pop up but the features that can invoke this problem are far more rare, are more self contained, and are easier to diagnose (i.e. template explosions which are localised vs the borrow checker which can be very much not localised).
The original comment was very much a critique of Rust and by no means some type of Rust exceptionalism.
> Languages like C, C++, or Ada ... make little to no attempt to enforce correctness
Both statements are laughably false, but for different reasons.
Both are based on the Doctrine of Rust Exceptionalism, which requires that Rust is not just a variation on a theme, but fundamentally different from other languages. Like most doctrines, this one is indefensible.
Rust compilation, like C++ and Haskell, is undecideable, not just NP-hard. Non-terminating compilation is artificially curtailed, thus failing to produce an open set of what would have been correct programs.
The Rust compiler performs certain correctness checks that other languages do not. It rejects an infinite set of correct programs that its correctness checks cannot resolve. In this as in all other particulars, Rust is very much on the continuum with other languages. All strongly-typed languages perform a huge variety of correctness checks, some built-in, others programmed, with great success, rejecting the large majority of incorrect programs people write. As a consequence, it is very common for Rust, C++, and Haskell programs to run correctly the first time, once the compiler is satisified.