Will Martin-Löf Type Theory lead to a greater ability to write provably correct code? This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory. 

The post makes the claim of a future 'unification' between the the describing language of math, and the operation based language of computer programming. 

My questions are:


Will these ideas lead to a better ability (through languages) to write provably correct code?
Have the full implications of MLTT been discovered on a theoretical level?
Does this post describe anything could couldn't already do in COQ or Agda?
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.