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
