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?