On Thursday, 23 October 2014 at 09:41:04 UTC, thedeemon wrote:
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,
Which is why I only suggest language-builtin-propositions on the
library level.
b) checking them requires turning your compiler into a
proof-checker,
I don't propose checking, as in an assert(). I propose to
assume() them and then run regular dataflow over the assumptions
that have been vetted by the library author.
Pretty close to what Walter wanted in the "assert as assume"
thread, but safer.
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.
That is true, which is why you have to do this at the high level,
and assume the worst.
To scare you well, here, for example, is my Smoothsort
implementation in ATS
http://stuff.thedeemon.com/lj/smooth_dats.html
Thanks! I'll look at it later, but note that I am not proposing
something like coq, ats or agda. No theorem prover.
What I am proposing is that libraries can provide assumed facts
about the result, then propagate those facts in the dataflow
until they have all become invalid.
properties. Writing it took me a few weeks. You don't want to
turn D into this mess. ;)
No, I want to turn it into a more pragmatic mess. ;-)
