Yes, I'm aware. However, like most such things, they're simply not practical. Proving compiler correctness is insanely difficult (if it wasn't, we'd have much better compilers) and it very frequently ignores optimization entirely, making such compilers useless.

In theory, proving correctness is a good way to go. In the real world, it's not remotely viable.