On Thursday, 31 July 2014 at 05:56:31 UTC, Walter Bright wrote:
On 7/30/2014 10:16 PM, bearophile wrote:
Walter Bright:
Show me a piece of code with different behavior. Start with
the array bounds
thing.
People have already shown you code that behaves differently
with assert and
assume.
I'd like to see what you are saying is different in a real
example.
But you have redefined "assert" to mean a mix of assume and
assert.
I haven't redefined anything. It's always been that way. It's
used that way in C/C++ (see your Microsoft C++ link).
No.
This is safe:
assert(x) {
if(!x) halt();
assume(x);
}
This is not safe:
assert(x){
assume(x);
}
You need to underestand what can be proven with Hoare logic. The
optimizer is free to do anything you can do with it.
A program + libaries contain millions of statements. Each and
every of those statements is taken as something close to an axiom
or multiple axioms. Basically your program contains millions of
implicit assumes() that are internally consistent.
Then you add thousands handwritten axioms of assume().
true == false IFF a single of those axioms contradicts another
axiom either provided implicitly by the program/optimizer or
explicitly by the user.
That means any boolean expression in your program+libraries can
be proven true or false randomly with a probability close to 100%.
That means you cannot do heavy duty optimization at all! Because
the probability of no axioms contradicting each other is very
close to 0%!
Please note that you can infer true==false if there is even the
tiniest teeny weeny sign of contradiction in any pair of axioms
picked from the millions upon millions of axioms provided. Even
if that axiom is derived from a statement deep down in some
library that most likely will never execute.
assume(X) provides axiom X
assert(X) provides theorem(X) to be proven
You cannot mix those two. That is disaster.
