What if your proof contains errors?
Your program is code, your proof is code, both are going to be buggy.
And what are you going to prove?
Your program is code, your proof is code, both are going to be buggy.
And what are you going to prove?
There was some discussion on the original post to HN about this announcement. In particular, look at this:
http://ertos.nicta.com.au/research/l4.verified/proof.pml
Which talks about the limits of provability.
In short, a "proof" that contains errors isn't really a proof of anything. And you build your proof inside an automated theorem prover so that it can be mechanically checked for internal inconsistency (i.e. contradictions), or for a completely inability to be false (i.e. tautologies).
If you understand a little bit about how something like Isabelle is constructed, only a small number of axioms are "hand coded", and then the rest is built from those. You can always build an external proof checking tool that checks that the proof you've constructed is correct. And if you're not confident in that, you can build another one.