D enters Tiobe top 20

Walter Bright newshound2 at digitalmars.com
Fri Nov 8 22:41:23 UTC 2019


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.



More information about the Digitalmars-d mailing list