Algorithms, term rewriting and compile time reflection

[bearophile via Digitalmars-d]

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