D enters Tiobe top 20

[Timon Gehr]

On 08.11.19 23:41, Walter Bright wrote:
> On 11/8/2019 8:10 AM, Doc Andrew wrote:
>> I am very bullish on formal verification in languages going forward. 
>> The one big advantage that D has in this arena is DbC. I was 
>> disappointed in your NWCPP talk that you listed it as a "miss." :) The 
>> potential here is huge! I think it's entirely possible that we can do 
>> _compile-time_ proofs that D contracts can be satisfied.
> 
> assert()s are the contracts that matter, not the in and out contracts, 
> which can be replaced with assert()s. In no way did I mean to imply that 
> assert()s were a mistake!
> 
> I've thought for 35 years that assert()s can be the input to a program 
> prover, i.e. it's nothing new, but I do not have the expertise to figure 
> out such proofs might work, other than simplistic cases.
> 

You need in and out contracts for modular verification.