On Sunday, 3 August 2014 at 22:57:24 UTC, Ola Fosheim Grøstad
wrote:
Turning asserts in program+libaries into globally available
axioms is insane.
I guess this is the heart of the difference in the way DbC
programmers program.
I know that program proving is impossibly hard, so my asserts are
a kind of short cut on it.
I use asserts to define my architecture.
So that I can say, "
In my architecture, I know, by design, certain eventualities will
never occur.
I don't expect any compiler to be able prove that for me
(although it would be nice if it could), but I certainly will be
relying on these facets of the architecture."
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.
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?
Of course it can, as every single line I write after the assert
is absolutely relying on the assert being true."
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."
And if the compiler chooses to rely on it too... I can absolutely
gaurantee you that differing optimizations will be the least of
my worries if the expression is false.
However, that said, it is very clear to me that this is a very
different usage of "assert" to what many of colleagues do.
Hence my suggestion we make explicit by differing names what
usage we mean.
Oh, and I will just thow this happy observation into the mix...
in case you think this sort of optimization is too
revolutionary... http://www.airs.com/blog/archives/120
