Not quite a problem as per se but it would be nice to have some kind of SMT solver inside a compiler to verify well-behaved-ness of certain functions. I'm not exactly sure whether you'd need something a bit more advanced for control flow analysis but beyond simple variable assignment checking (imagine Ada style bounds) I would quite like a language with a verifier like eBPF uses to reduce bug surface area (i.e. Not all code needs to be Turing complete). I think there are langauges with features like that but none aimed at mainstream use beyond research and/or defence etc.

I would like to write a language like that but I don't know enough about computer logic / hard ai etc. to know where to go in terms of the internals of the compiler (Bolting complicated analysis onto an existing compiler is really really ugly if there is a lot of global state - e.g. some parts of the D compiler although that's still WIP to be fair to the programmers)