> Can you give an example of this?

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.

The reason that you found the specification of a sorting algorithm simpler than the sorting algorithm is that you probably have not fully specified the algorithm. Consider the sorting algorithm in C's standard library, which allows the user to specify a comparison function. Now imagine you'd pass something like the following comparison function:

   def compare (x, y):
      printf ( "I'm comparing %i with %i\n", x, y )
      if ( x < y ) return 1
      if ( x == y ) return 0
      else return -1

It almost completely exposes the inner workings of sorting. Hence a full spec needs to account for this.

> 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.

Check out the article(s) about Amazon’s use of TLA+ for a good, industrial example of formal methods:

http://lamport.azurewebsites.net/tla/amazon.html