I don't understand why the entire known software corpus is not automatically proven yet. Computation is a very strict process. I'm not talking about a computer writing code itself, but a programmer should write programs using some formal language and the computer should be able to follow the proof. I.e. no bugs.

/s