But then there's no such thing as an unannotated program. I'm confident in my ability to prove things the old-fashioned way, using brain, pencil and paper, so I

But then there's no such thing as an unannotated program. I'm confident in my ability to prove things the old-fashioned way, using brain, pencil and paper, so I don't see much value in merely having my proofs verified by a machine. If the machine can't contribute to the effort of actually coming up with the proof, it should stay out of the way.