[seanwilson]

> It's pretty clear that a fully formal specification of a program must be (roughly) as complex as the program itself, for otherwise you could construct an infinitely descending chain of ever simpler specifications which leads to a contradiction.

That's like saying a theorem statement must be roughly as complex as the proof.

Also consider that it's much harder to reason (and prove) that heavily optimised versions of algorithms are correct compared to naive implementations. For example, a proof of correctness for heapsort is more involving than one for insertion sort.