Comment by fooker
4 hours ago
> There's no point in hoping that somehow Programming Languages will overturn Mathematics.
Maybe you misunderstood my point?
Getting rust to a more complete state would be overturning mathematics here, as you note you can’t have both soundness and completeness.
What I say does not require overturning mathematics, ie allow unsound programs to compile but have different methods of catching them, both statically or dynamically.
Rice's Theorem says we can advance arbitrarily close but can't reach the goal of compiling exactly the set of correct programs (all correct, none incorrect). Some years ago Rust landed "Non-lexical lifetimes" borrow checking which is an example of such an advance, you don't need to overturn mathematics to make such advances, only to reach the goal. Work to further improve lifetime checking is ongoing though I doubt anything as big as NLL is on the foreseeable horizon.
The problem isn't directly with C++ choosing "All correct programs compile" but instead with the resulting incentive structure. Programmers want their program to compile.
In Rust the incentive is to improve the compiler, allowing more programs (all of them correct) to compile as with the NLL changes.
But in C++ the incentive is to loosen the requirements, allowing more programs (some of them incorrect) to compile, as with Concepts Lite in 2020.