On Tuesday, 5 August 2014 at 10:00:55 UTC, eles wrote:
It is wise to mix them to such degree as to no longer distinguish them? For me, assume and the like shall rather go with the annotations.
That's one of the reasons I think it is not new territory, since letting assert have side effects basically sounds like constraints programming/logic programming.
I do think that constraints programming has a place in support for generic programming and other things that can be known to evaluate at compile time. So I think imperative programming languages are going to become hybrids over time.
Also, if you think about the new field "program synthesis", where you specify the constraints to generate/fill out boiler code in an imperative program, then the distinction becomes blurry. Rather than saying sort(x) you just specify that the outcome should be sorted in the post condition, but don't care why it ended up that way. So the compiler will automatically add sort(x) if needed. Sounds like a powerful way to get rid of boring programming parts.
Another point, when you think about it, Program Verification and Optimization are conceptually closely related.
S = specification // asserts is a weak version of this P = program E = executable ProgramVerification: Prove( S(x)==P(x) for all x ) Optimization Invariant: Prove( P(x)==E(x) for all x )
