Microsoft is stupid enough since the first decision of the implementation impacting the ABI is made. There was no one enforcing such bad decisions shipped into the productions at the very beginning.
Both libstdc++ and libc++ have more flexible rules to preventing ABI breakage.
In some stricter sense, back-end is for target-depending stuff like ISA-dependent code generation. A great deal of work in both GCC and LLVM is in the so-called mid-end. Both have more than one IRs in the pipeline after the front-end.
This is technically incorrect. A programming language can be designed with specification in mind, even with a formal one (e.g. SML). It is just true that the specification is not likely effectively verified before more than one real implementations landed, if it is not formally verified. (Anyway, verification by testing of existing implementations _is_ the fallback where people cannot afford the cost of formal methods.)
There are simply lacking of such strong requirements in language standards. C/C++ even have the specific "linkage" concept to abstract the binary details under the source form away. And you may know, many libraries are distributed by binaries.
The standards implying binary compatibility rules are about ABI (application binary interface), which usually depend on the ISA (instruction-set architecture) or the OS (if any) being used. You cannot have the unique one once there are multiple ISAs/OSes supported. Even when you only want to rely on some external "exchanging" representations not tied to specific ISAs, there are already plenty of candidates: CLI, JVM, WebAssembly... Plus there are more than one executable (and mostly, runtime loadable) image formats widely used (PE/COFF, ELF, Mach-O ...). You will not have the unique combination, and any attempts to ensure it "work across compilers" in that way will likely finally just add a new instance not fully compatible to existing ones, making it more fragile.
It's about the ability, not the reality. As Racket, the base language can have no explicit rules for any type systems to be embedded. There can be more powerful candidates, e.g. Kernel: https://web.cs.wpi.edu/~jshutt/kernel.html.
Racket is special because its designers provide dedicated support of language-oriented programming. But that is about ecosystems, not typesystems.
Types are closed terms of contracts encoded in a language within specific phases. If you really need any guarantees without further knowledge shaped before running, then, besides the typechecking, the typing rules should also be programmable by users (rather than the language designer) for the sake of providing proofs. The base system must practically have no mandated static type systems at all, which is far from Rust.
I'm disappoint to "VM-like" behavior too, so I don't expect they would be totally replaced by WSL.
But this is similar in the other direction. Many applications just rely on such "VM-like" behavior, even though they can be (re)built for Win32 and/or they do not need a real VM for functionality. Note WSL1 can already do something more, e.g. hosting programs as X clients working with VcXsrv. I don't think WSL2 will be necessarily better than WSL1 in many of such cases. (In particular, when I have to reserve VT-x for some other hypervisors, I have no other choice.)
Microsoft is stupid enough since the first decision of the implementation impacting the ABI is made. There was no one enforcing such bad decisions shipped into the productions at the very beginning. Both libstdc++ and libc++ have more flexible rules to preventing ABI breakage.