Algorithms, term rewriting and compile time reflection

[thedeemon via Digitalmars-d]

On Tuesday, 28 October 2014 at 01:10:18 UTC, Andrei Alexandrescu 
wrote:
> 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

Here's one in Agda:
http://twanvl.nl/blog/agda/sorting