I just wanted to ask if it would be possible to construct a language with a type system that can solve the memory management problems (memory leaks, dangling pointers, double free(), etc.) by automatically trying to prove the correctness of any program with its types as propositions like with an integrated coq-like theorem prover (in the mindset of programs as proofs)?
Is there a fundamental logical problem to this approach (halting problem maybe?) or is it just unfeasible? Thanks for any answers and I'm sorry that I'm not so well-versed in this field, just want to know out of curiosity ;)
Yes, there has been a lot of research into languages that do compile-time memory management. Rust and its ownership model is the most high profile industry language in this area. You might always want to look into "linear types".