bearophile wrote:
Given that pre-conditions are meant to run fast and to be (nearly)
pure, this is my idea: when you call a function with all arguments
known at compile time (as at the r3 variable) the compiler runs just
the pre-condition of that function at compile-time (and not its body
and post-condition).
The advantage is some bugs are caught at compile-time, and the
compiler is kept simple (I'd like contracts to be verified statically
in more situations, but this requires a more complex compiler). The
disadvantage is longer compilation times, and troubles caused by
pre-conditions that can't really run at compile-time (like a
precondion that uses a compiler intrinsic). A way to solve this last
problem is to not raise an error if a pre-condition can't run at
compile-time, and just ignore it, and let it later run normally at
run-time.
We thought about this approach and deliberately did not do it.
It is not predictable at compile time whether a function can be executed
at compile time or not (the halting problem). Therefore, you'll wind up
with cases that silently fail at compile time, and so are put off until
runtime. The user cannot tell (without looking at assembly dumps) if it
happened at compile time or not.
Instead, we opted for a design that either must run at compile time, or
must run at run time. Not one that decides one way or the other in an
arbitrary, silent, and ever-changing manner.
The user must make an explicit choice if code is to be run at compile
time or run time. D has had this in operation for several years, and
it's been a big success. I don't think we should tamper with the formula
without very compelling evidence.
