assert semantic change proposal

[via Digitalmars-d]

On Sunday, 3 August 2014 at 23:54:46 UTC, John Carter wrote:
> I know that program proving is impossibly hard, so my asserts 
> are a kind of short cut on it.

Yes, but the dual is that writing a correct program is impossibly 
hard. A correct program works as specified for all improbable 
input and configurations. No shipped programs are correct.

However, if you turn asserts into assume, you let the compiler 
use any defect in the program or the specification to prove 
"true==false". And after that all bets are off.

With asserts on, you can tell where the flaw is.

With asserts off and logging on you can figure out where the flaw 
is not.

With asserts turned to assumes, no amount of logging can help 
you. You just know there is a flaw.

Worse, an improbably occurring bug can now become a probable one.


> When I assert, I'm stating "In my architecture, as I designed 
> it, this will always be true, and everything in the code 
> downstream of here can AND DOES rely on this.

But it does not matter if it holds. The deduction engine in the 
compiler is not required to limit itself to the location of the 
"assert turned into axiom". It can move it upstream and 
downstream.

It is also not only a problem of mismatch between two axioms, but 
between any derivable theorems.

> My code explicitly relies on these simplifying assumptions, and 
> will go hideously wrong if those assumptions are false.... So 
> why can't the compiler rely on them too?

Because the compiler can move them around and will assume all 
improbable configurations and input sequences.

> Of course it can, as every single line I write after the assert 
> is absolutely relying on the assert being true."

Yes, but the axioms can move anywhere. And any contradiction 
derivable from any set of axioms can lead to boolean expressions 
turned to random values anywhere in your program. Not only near 
the flawed assert turned into an axiom.

> My asserts are never "I believe this is true".
>
> They are _always_ "In this design, the following must be true, 
> as I'm about to code absolutely relying on this fact."

Yes, but if you state it differently elsewhere, indirectly 
(through a series of axioms), you may have a contradiction from 
which you can deduce "true==false"

Please note that any potentially reachable code will be included 
in the axiom database. Not only the ones that will execute, also 
branches that will never execute in a running program.

Those can now propagate upwards since they are true.

Almost no shipped programs are correct. They are all wrong, but 
we take them as "working" because we don't push them to extremes 
very often.

Let me quote from the CompCert webpage:

http://compcert.inria.fr/motivations.html

<<More recently, Yang et al generalized their testing of C 
compilers and, again, found many instances of miscompilation:

We created a tool that generates random C programs, and then 
spent two and a half years using it to find compiler bugs. So 
far, we have reported more than 325 previously unknown bugs to 
compiler developers. Moreover, every compiler that we tested has 
been found to crash and also to silently generate wrong code when 
presented with valid inputs. (PLDI 2011)

For non-critical, "everyday" software, miscompilation is an 
annoyance but not a major issue: bugs introduced by the compiler 
are negligible compared to those already present in the source 
program. >>