On 10/28/14 2:26 AM, bearophile wrote:
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
Looks like the one I saw years ago: a proof that you don't want that
kind of stuff :o). -- Andrei
