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.