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