On Tuesday, 29 July 2014 at 20:07:16 UTC, Timon Gehr wrote:
He still has a point. This is just another case of the keyword not matching the semantics very well. It would be more aptly named 'assume' instead of 'assert' (and be un-@safe if release mode is to trust it unconditionally.)
But you cannot check preconditions, postconditions and invariants with an assumption!
Assumptions does not have to be checked. They have to be proved. And preferably formally verified. Sure, it might be nice to have 2-5 assumes() in a program to boost optimizers where it fails. Without a proof of correctness? Insane!
Seriously, have anyone EVER read a programming book where all examples worked? And those are tiny toy programs and vetted.
Heck, even Ole-Johan Dahls book on Verifiable Programming, with Hoare as editor had a fairly long errata. And it was carefully written.
Anyway, if you cannot assert() with headroom then you cannot use assert loop invariants in many floating point algorithms.
There are plenty of sources of indeterminism in a real execution environment, so anything more than very limited partial correctness is a pipe-dream for any complex interactive program.
Only if you assume _a priori_ the program to be correct.
Which is insane. Having 2-3 carefully crafted assume() and 500 assert() would be ok (but I am in doubt of even that). Having 500+ assume() is crazy.
