On 8/2/2014 12:00 AM, Chris Cain wrote:
It is not so clear where to draw the boundaries. In some languages you may
need to prove the assertion true in order for it to pass the type checker.
That would be a cool construct as well, don't get me wrong. But considering the
vast majority of programs could not reasonably have such proofs, I think the two
concepts are orthogonal. I'd rename that to a "prove" statement and not an
"assert" because assert has nothing to do with checking and conflating the two
has caused confusion.
I think at this point it is quite clear that D's assert is about the programmer
saying this expression evaluates to true or it's a programming bug.
If other languages use assert to mean "the compiler must prove this to be true"
then that's fine for those languages, but it isn't what D's assert is, or can
ever be.
I.e. I agree with you.