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)
In recent years there has been a lot of improvement in refinement types which is, from what I understood, what you are describing. See for example Liquid Haskell that uses Z3 solver for static verification.
I'd say that when dependent + refinement types get more mature and get pass the basic prototype idea in research languages/environments, these ideas could easily transfer to mainstream static typed languages and be a new module of future compilers.
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)