Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
I don't think your question is particularly well posed. It mostly asks for opinions. Here are mine:


Yes.
I do not know what you mean, but the answer is probably "there is more MLTT theory to be done, although we do know a lot".
You cannot do all of homotopy type theory in Coq and Agda. This is an active area of research.