I have this same discussion with folks applying formal methods to prove the correctness of software where I work. Often the "proof" is harder to read than the original code and I certainly don't feel anyone has proven anything to me.