D enters Tiobe top 20
x at x.com
Sat Nov 9 02:43:41 UTC 2019
On Friday, 8 November 2019 at 22:41:23 UTC, Walter Bright wrote:
> 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.
Now you've done it. I've seen this before, right before templates
were in D. This is where you disappear for a couple of weeks and
then come back to announce that D can formally verify user code,
The in/out syntax doesn't add a lot for typical function body
code, since everything is in sequential order anyhow, but in
interfaces they would be essential. They may be under-utilized,
but I think they might just be one of those features that is a
late bloomer. I wouldn't consider taking them out of the language
just yet, even for regular functions.
Proving properties of D code outright is probably tough, but
doing a mechanical conversion (of at least some subset of D,
maybe betterC) to an intermediate language like ML and then
feeding it into a solver is probably possible. Here's an
interesting project I found that can generate Why code from
LLVM-IR: https://github.com/AnnotationsForAll/WhyR. It might be
interesting to throw some LDC IR at it and just see what happens!
Given that D already has contracts in place, using them to
generate Why's "ensures" and "requires" clauses would be much
easier than something like C where you'd need specially-formatted
comments or a language extension.
Even without specific contracts, a list of things that you _know_
are run-time errors (divide-by-zero, null-pointer dereference,
etc.) could be proven absent from code. The nice thing about an
approach like this is that you don't have to change the language
or mess with the compiler, instead the prover is just another
tool, like a linter, that you can use if you need it.
Not everybody is as optimistic as I am, but I do believe that
with the emphasis on safety these days, I suspect FV will become
a requirement in the future.
More information about the Digitalmars-d