Andrei Alexandrescu:
I recall there was an earlier implementation of a statically-checked sort, maybe in Agda? It wouldn't typecheck if the output array weren't sorted.
Yes, there is a similar code even in ATS language (that is much simpler than Agda, you can't verify a generic proof as in Agda), this is a verified QuickSort-like on lists (I don't remember an equivalent verified QuickSort on arrays in ATS):
http://dpaste.dzfl.pl/e60eeb30e3b6 Bye, bearophile
