D enters Tiobe top 20
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Sat Nov 9 17:16:40 UTC 2019
On Saturday, 9 November 2019 at 14:49:32 UTC, Doc Andrew wrote:
> As a stop-gap we might be able to use an
> @assume UDA, but I do think "assume" could be added as a
> reserved keyword in the near future in anticipation...
True, I meant to refer to the concept, not syntax. Maybe the
syntax for assume should be ugly enough to really stand out so
that it is caught in reviews, "@ASSUME" or "@__assume"... Dunno.
That is a detail, though.
> I like the idea of having a compiler flag to treat assumes as
> asserts, maybe even in release mode?
It could at least be useful in cases where you do exhaustive unit
testing (test all combinations), then assume would be safe.
>> This allows you to get started working on the optimizer and
>> figure out how to make good use of the extra facts.
>
> That's probably a much longer-term goal, but just being able to
> move normal error-checking into contracts and depending on them
> in release code is a big win IMO.
Well, not necessarily, some C++ compilers support it. The
problem is that you probably don't want to introduce too many
auxiliary facts, as that would just slow down compilation with no
gain (and perhaps even confuse a naive optimizer). Anyway, you
should be able to add facts to LLVM by compiling a boolean
expression and then assuming it to hold.
But maybe the language syntax should allow you to select which
propositions you want to propagate to the optimizer. Not sure if
LLVM can express quantifiers though (forall/exists).
> This might be more difficult to enforce without some tight
> compiler integration. An attribute like @ensured or @certified
> could be the "gold standard" of safe D code, which would
> require a proof of no run-time errors and all contracts.
> Without the proof, the compiler could throw an error for
> functions with this attribute.
Well, that might be an issue, if the ensure-statement is meant to
help optimization then it could simply be omitted. If it is meant
to help correctness then it could be translated into an assert if
it isn't verified.
But I guess one will have to distinguish the two cases somehow.
Which is basically why I think trying to improve basic libraries
with assume-statements and manual proofs is the best starting
point. Then you get an idea for how it can affect optimization.
You probably also want to bake into a certificate trust-building
meta information, such as which verification method, and who did
it and where, so that developers can specify constraints like
"must be verified by service X using verifier Y or Z". Or open
up for hand-verified code by developer Q or a specific
organization (could be a URL to a public-key).
> We'd probably need a DIP to hash this out.
I will certainly read and comment on it, if you want to write
one. You could start with specc'ing out a list of requirements?
> This might tie in with some of the work going on with
> reproducible builds, but I love the idea of certs for known
> good object files.
I actually meant source code only. You distribute the source
code, but with certified "requires"/"assume"/"ensures" statements
that is bound to the source code using cryptographic hashing and
an online index (so that it can be checked or revoked).
I guess one issue is that it has to be a standalone library (e.g.
only depend on a specific version of the standard library) for
this to work. Otherwise you would have to tie it to a specific
certified version of all the libraries you depend on.
But... I don't actually think that is a big deal, you typically
would pre-verify basic libraries. You could use a simple
concatenation for the hash with sorted filenames and some
sentinel character sequence for separating files, e.g.:
filename1, sep, file1, sep, filename2, sep, file2, sep, sep.
> Using something like the @certified (or @ensured, or @verified,
> or whatever) attribute, we could just turn off run-time checks
> in these functions if a proof exists, could be as simple as a
> source.d.proof file with the function name (and hash?) in it.
I am actually not sure how this could be done well. Because you
could have array accesses within a conditional expression.
Maybe you'd actually have to annotate the indexing with some new
syntax to tell the compiler that the access does not need bounds
checks as it has been proven already to hold... So I guess this
is an area that needs to be fleshed out with many examples.
Anyway, it seems reasonable that a tool would take source code,
verify it and emit an annotated version of the source code. Then
less capable compilers could use the verified results.
Most users are not going to write verifiable code themselves.
> I'm not sure about this one. Usually assumes are big red flags,
> they're the FV version of unsafe - "trust me, I know what I'm
> doing", that sort of thing. I might have misunderstood your
> intent here though.
I think so, if they are proven to hold by a tool/compiler then
they hold. Dataflow analysis is sufficient, when it succeeds, but
will fail in many cases at it is a weak approach. However, it is
also much faster than a proper solver. Basically just an
optimization for performance reasons.
But you also want to use assume manually sometimes when
describing hardware registers (e.g. describing that bit 8-32
always are zero), or when something has been proven by hand and
has a significant performance impact.
> This is how SPARK works, even if you can't prove a (normal Ada)
> function body, because of inline asm, or pointer arithmetic or
> something, you can still specify pre and post-contracts on the
> interface. I think there's a little bit of a @trusted feel to
> it, since the post-conditions on a non-SPARK function become
> sort of an assumption that the function does what it claims,
> given the preconditions hold. I think SPARK may leave these as
> run-time checks (normal Ada behavior, normal D _Debug_
> behavior), which you'd have to do to have any sort of
> confidence in your proof.
Yes, for typical SPARK use cases that seems reasonable.
> This is where things get a little messy. Verified functions
> calling non-verified functions with post-condition checks would
> need these checks enabled even in release mode, I would think.
Yes, this is where different goals may lead to different
designs... so the challenge is to come up with something that can
both support correctness and optimization without being extremely
complicated in terms of syntax.
> The cool thing is that D _today_ has all the syntax it needs to
> start working on tooling for this with no language changes.
Sure, you could also just define a dummy "ensures", "requires",
whatever… function that takes a boolean as a parameter. With an
empty body, or an assert.
> a particular build. I'm not as concerned as some are with
> proven builds and linking, but there may be high-integrity
> requirements in the future where this sort of thing is
> required. I'm not sure if it's a thing yet, maybe NASA does it,
> but I'd be surprised if anybody else is yet.
There are papers on proof-carrying-assembly code...
Although the basic idea behind certification would be that you
get to use the postconditions and assumes without having to run
costly verification on your own machine.
You might even see a commercial service with very strong provers
and effective hardware.
> I'm not totally familiar with the landscape, but generating
> Why3ML from D seems like it would be one good way to start. You
> get access to a lot of solvers for free, it seems like it's
> well-documented and fairly easy to use.
Perhaps Why3ML is a good choice, but I would've started with
Boogie.
More information about the Digitalmars-d
mailing list