Algorithms, term rewriting and compile time reflection

[Andrei Alexandrescu via Digitalmars-d]

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