Comment by adrianN

I don't think anyone wants elegant proofs for their software's correctness. As long as the code is proven correct, programmers would be satisfied.