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

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

Sound like madness :) I'd love to see it.

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

> http://dpaste.dzfl.pl/e60eeb30e3b6

That code is in ATS1. Now there is ATS2 that has a better syntax, and is a bit more powerful (and can compile even to JavaScript). On the ATS site all the ATS1 examples apparently have being removed.

Bye,
bearophile

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

On 10/27/14 6:53 PM, deadalnix wrote:
> 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
>
> Sound like madness :) I'd love to see it.

Looked again for it, couldn't find it. Got this other one instead:

http://lara.epfl.ch/~psuter/articles/BlancETAL13OverviewLeonVerificationSystem.pdf


Andrei

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

Andrei Alexandrescu:

> Looks like the one I saw years ago: a proof that you don't want that kind of stuff :o). -- Andrei

Silly Andrei :-)

Bye,
bearophile

On Tuesday, 28 October 2014 at 09:26:35 UTC, bearophile wrote:
> 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

Quick sort and insertion sort is relatively easy to prove correct using induction:
1. prove termination
2. prove output is permutation of input
3. prove that the processed units are sorted (left part in insertion sort)

But this is not what I am suggesting in this thread. This is not meant for application level code, but for libraries and compiler.

So rather than proving property 2 and 3 it should just be provided as facts from the library, then the compiler will propagate that knowledge through the call graph until it has been deemed uncertain.

For instance if you have asserted that a value exist in an array, then that knowledge will hold for all permutations of that array further down the call graph.