You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet
As I understand it, creating a proof becomes increasingly more complex in proportion to program size. You'll notice in this project, their proof only covers a few hundred lines of code. That's not because their program just happened to be a few hundred lines of code, but because they designed it to allow a practical proof.
The theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.
As I understand it, creating a proof becomes increasingly more complex in proportion to program size. You'll notice in this project, their proof only covers a few hundred lines of code. That's not because their program just happened to be a few hundred lines of code, but because they designed it to allow a practical proof.