Algorithms, term rewriting and compile time reflection

[via Digitalmars-d]

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