D enters Tiobe top 20

[Walter Bright]

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

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.