I don't think that the goal here is to show a fast and elegant sort, but rather to show that a sorting algorithm that seems like it can't possibly work actually

I don't think that the goal here is to show a fast and elegant sort, but rather to show that a sorting algorithm that seems like it can't possibly work actually does. That is, probably no-one will learn from this article how to sort better, but hopefully people will learn from this article how to formally prove things (e.g., about sorting) better.