On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
This is an assume, not an assert.
Not sure what you mean. An assume is an assert proven (or defined) to hold. It can be a proven theorem which has been given the status of an axiom. It is known to keep the algebraic system sound. If you claim that something unsound is proven then all bets are off everywhere?
I am quite confident that assume(false) anywhere in your program is basically stating that the program is unsound (true==false) and should not be compiled and run at all. If true==false anywhere in your program then it surely holds everywhere in your program?
The only reason c-style assert(false) "works", is because you delay the verification until the last moment, at which point the system says "woopsie", gotta terminate this because this program should never have compiled in the first place.
Sounds consistent to me?
