[fdupress]

Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn't just drop values or fill the entire array with 0s (with fixed-length arrays, as here).

On paper: "it's just swaps" Formally: "how do I even specify this?"

(For every value e of the element type original array and the final array have the same number of occurrences of e. Show that that's transitive, and show it's preserved by swap.)

[touisteur]

Hi, co-author here. We actually touched upon this subject in the article: 'Tip: Don’t prove what you don’t need to prove' and surrounding text. Also previous comment by Yannick: https://news.ycombinator.com/item?id=31980126

[fdupress]

Looked for it and missed it.

And thanks for writing this up, by the way. Having people less familiar with formal methods try and write up their experiences is, I think, much more effective at letting people in than having experts try and write tutorials.