D enters Tiobe top 20
newshound2 at digitalmars.com
Tue Nov 12 11:31:43 UTC 2019
On 11/12/2019 2:26 AM, Timon Gehr wrote:
>> At runtime Assert and Assume behave the same: If the condition is false, then
>> the program fails – how it fails (e.g., throwing an exception, opening a
>> dialog box, etc. can be completely customized with CodeContracts)."
>> Therefore after the Assert, the prover can assume the Assert condition is
>> true. If the prover can prove the Assert is always true, the runtime check can
>> be safely removed.
> (Technically, probably no, as last time I checked, the code contracts prover
> still implicitly assumed there cannot be integer overflow.)
D doesn't have a contracts prover, and if it did, I think it would be a mistake
to ignore integer overflow. What would be of value is being able to prove
integer overflow does not happen. Note that the Value Range Propagation logic in
D is able to do some nice work that does take into account overflows.
The global optimizer data flow analysis I wrote long ago would be broken if it
didn't concern itself with overflows. In particular, loop induction variable
optimization wouldn't work.
> Maybe, but in D assertions get converted into optimizer assumptions in release
> mode _without_ any such proof being provided.
True, but D doesn't have a prover anyway :-)
The user has complete control over whether asserts are checked at runtime or
not. The thing about -release mode is the result of being bludgeoned in the
press for having "slow" code because a competitor didn't generate the checks and
the ignorant journalist did not understand this and did not ask before going to
I last tried Spark many years ago, and discovered its contract prover was so
limited I concluded it had little practical value. (If I recall, it couldn't
deduce things like odd and even.) I'm sure it has improved since, but how much,
I have no idea.
More information about the Digitalmars-d