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