Algorithms, term rewriting and compile time reflection

[Andrei Alexandrescu via Digitalmars-d]

On 10/23/14 2:41 AM, thedeemon wrote:
> To scare you well, here, for example, is my Smoothsort implementation in
> ATS
> http://stuff.thedeemon.com/lj/smooth_dats.html
> that includes proofs that the array really gets sorted and the Leonardo
> heaps used in the process have proper form and properties. Writing it
> took me a few weeks. You don't want to turn D into this mess. ;)

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.

Andrei