assume, assert, enforce, @safe

[via Digitalmars-d]

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 )