D enters Tiobe top 20

[Timon Gehr]

On 12.11.19 12:31, Walter Bright wrote:
> 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.

(Sure. Just saying that is what their prover does, so you actually can't 
eliminate the check based on that.)

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

(I know. I contributed some code to that.)

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

It's funny you would bring that up, because it indeed does not work:
https://issues.dlang.org/show_bug.cgi?id=16268

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

Yes, it does, just not for functional correctness. D has a @safe 
fragment where the compiler automatically proves absence of memory 
safety problems. asserts are allowed in @safe code. Assuming incorrect 
propositions in your optimizer can cause memory corruption. See the problem?

> The user has complete control over whether asserts are checked at 
> runtime or not.

No. You either check, or you risk UB. Complete control looks different.

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

Well, now you can be bludgeoned in the press for having "unsafe" code, 
because the ignorant journalist called into some library with an 
assertion in it. Even if they decide to ask, your response would make 
their article more juicy, not less.

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

I never tried Spark and it's entirely plausible that they were/are 
vastly behind the state of the art in verification research.