[JadeNB]

> After the first main loop, the first item will be the biggest item in the list.

> The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

I think the "and so on" is the point. To put it more precisely, I think that anyone (with a suitable familiarity with the tools) can prove formally that "after the first main loop, the first item will be the biggest item in the list"; but I think that it might take a bit more work to prove the "and so on" in a way that satisfies a formal prover.

(As to the intuition—I can buy that the "and so on" part is reasonably intuitive, but only at a level of intuition that can also believe wrong things. For example, just always replacing bigger items with smaller items doesn't guarantee you'll get a sorted list!)

[MattPalmer1086]

Sure, formal proof would be a lot harder. I just didn't find it quite as surprising that it works as the article implied.