D enters Tiobe top 20

[Timon Gehr]

On 12.11.19 10:12, Walter Bright wrote:
> On 11/11/2019 8:25 PM, Doc Andrew wrote:
>> I think _most_ people consider Assert vs Assume the way SPARK and F* 
>> do - as seen here: 
>> https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 
> 
> 
> Which says:
> 
> "Intuitively, Assert is something that you expect the static checker be 
> able to prove at compile time, whereas Assume is something that the 
> static checker can rely upon, but it will not try to prove.

Here, I was talking specifically using verification terminology, where 
the difference is obviously night and day. Then you dismissed my post by 
claiming in D they are the same. You might as well declare that from now 
on true is the same as false in D and hence you can reach any desired 
conclusion, but that won't change my understanding of logic, nor would I 
applaud your design choice.


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

Maybe, but in D assertions get converted into optimizer assumptions in 
release mode _without_ any such proof being provided.