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.
