Well, you can do that in traditional languages as well, just wrap your list in a SortedArray type. Chances are your “sorted” function won’t actually prove the

Well, you can do that in traditional languages as well, just wrap your list in a SortedArray type. Chances are your “sorted” function won’t actually prove the algorithm used formally either in a dependently typed language.