Algorithms, term rewriting and compile time reflection

[thedeemon via Digitalmars-d]

On Wednesday, 22 October 2014 at 23:09:17 UTC, Ola Fosheim 
Grøstad wrote:

> I  would always assume it has been done plenty of work related 
> to proving properties about a program since this is the holy 
> grail of CS!
>
> I think it is related to so-called dependent types?
> http://en.wikipedia.org/wiki/Dependent_type

Yes, dependent types allow expressing properties like the ones 
you describe. However
a) it's not easy at all even for simple data structures, often 
requiring defining many additional types and lemmas,
b) checking them requires turning your compiler into a 
proof-checker,
c) what works in "clean room" (like high-level total functional 
language) is hardly feasible in a "dirty" language like D where 
you can go as unsafe as you want.

> I'd like to take a look at Xanadu some time…
> http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html

That's obsolete, I guess, better take a look at ATS language from 
the same author. It's really really close to what you're thinking 
of here, minus the rewriting.

> And Agda which also guarantee termination!
> http://en.wikipedia.org/wiki/Agda_(programming_language)

Yep, all dependently typed languages like Agda, ATS or Idris 
require the functions you use in types to be terminating 
(otherwise your proofs become unsound and worthless) and they all 
include termination checking.

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. ;)