Algorithms, term rewriting and compile time reflection

[via Digitalmars-d]

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.