D enters Tiobe top 20
x at x.com
Sun Nov 10 02:51:53 UTC 2019
On Sunday, 10 November 2019 at 00:27:46 UTC, Ola Fosheim Grøstad
>> - Universal quantification: The low-impact way would be to set
>> aside an attribute @forall or @foreach, then figure out what
>> tuple elements you'd need to generate a VC from them and how
>> you'd tie them to a function, module, variable, etc.
> I was more thinking, what do you do if it fails? One cannot
> keep O(N) or O(N^2) asserts in the code as a dynamic check...
> I guess the easy solution is to require that "ensure" is
> fulfilled at compile time and not allow quantified expressions
> in asserts.
Yeah, you could make ensure work like assert but strictly for
proofs and not at runtime, but I kind of like the idea that if
you can't prove a check at compile-time, it still makes it into
your Debug code for thorough testing.
For the most part you're back to the status quo when a proof
fails - you've got some unit tests to write, the checks will live
in Debug code and they'll go away in Release code just like they
do now. If the Debug performance hit is too onerous, then comment
it out, or have a separate "proof-time assert". I'd have to think
The one thing I'm not sure about is the situation I hinted at
where post-conditions are on an interface where the function body
itself wasn't proven. In this case, maybe they just act like
assumptions. I have to do some more homework here.
> I once added a unicode-token-layer to the dmd-lexer, and added
> alternative unicode math symbols to expressions. It only took a
> few hours. Modifying the lexer is a lot easier than expanding
> the parser. I think people who would write VC also would be
> familiar with math notation, so I one could just use that to
> avoid clashes.
> E.g. you could have a not-so-pretty ascii syntax and a unicode
> Like: "∀" vs "@vc_forall"
> Unicode tokens is really easy to do this way as you just can
> rewrite "∀" to "@vc_forall" and "∃" to "@vc_exists", so no
> major changes are needed to add unicode symbols.
You're going to scare people off with that sorta stuff :)
> Proving loop progression and termination is very important, and
> not so easy. What some FV languages do is that they introduce
> ghost-variables for this (variables that are conceptually
> computed but not used for code generation).
> So basically you increment the ghost variable(s) every
> iteration and prove that there is a threshold for the value
> where the loop terminates.
> But it won't really change the language that is compiled. It
> only changes the language that is verified. So not an effective
> But verification will probably have to happen after template
> expansion... Not sure how to deal with that. Unless you want
> to verify templated code... which would be cool, but not sure
> of what roadblocks you would hit.
Yeeeah... I'm not sure how that is going to play out. I don't
really know how contracts work with templated code currently. It
could be that if the contracts appear in template code, then they
just get copy-pasted into each new instantiation of the template,
and life is good. The prover will do a ton of extra work
re-proving the same thing for each new type, but who cares? And
actually, you might discover that the perfectly generic function
you wrote actually has a bunch of nasty corner cases lurking
I think you'd just have to wait until all the CTFE and template
stuff is done before you start generating VCs. It might not be a
deal-breaker, but that's speaking from ignorance, frankly.
> Lots of potential with more advanced typing... but prepare to
> be met with a lot of resistance for things that are actual
> language changes (things that can affect code gen and not only
> the verifier).
Oh yeah, I'm not holding my breath for anything like that. Baby
> Well, yes, but not necessarily a language change... As a start
> you could just define a local function "__vc_invariant" and
> treat it special by the verifier?
True, we might be able to just use a nested function with some
contracts baked into it.
> If you write up something formal you ought to list such
> use-cases, and what they require.
>> The goal is that a user doesn't have to do anything different
>> than normal to write verifiable code.
> :-/ not possible though.
Oh I dunno, aside from adding some extra contracts and avoiding
certain language constructs* (like goto), not much really has to
change for the average user to get some benefit from running the
code through a proof tool, even if they could care less about
stamping a function as "certified" or not.
* Granted, those "certain language constructs" may end up being
an insurmountable barrier, where the formally verifiable subset
of D is stripped of so many features that it isn't really worth
it. Too early to tell.
> But you'll get feedback on whether there is any interest at all
> in the community? If there is no interest then it would not be
> possible to maintain it in the compiler either.
> Starting a discussion on the vocabulary might tell you
> something about what kind of support you can expect for your
Let me mull it over a bit. I might start a separate thread where
people can weigh in. The field is still pretty new [AI/ML 70
years ago ;) ], so it might be a good way to raise awareness and
at least get people thinking about some of the possibilities for
writing _real_ safe code.
More information about the Digitalmars-d