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. >>
