D enters Tiobe top 20

[Doc Andrew]

On Sunday, 10 November 2019 at 00:27:46 UTC, Ola Fosheim Grøstad 
wrote:
>
>> - 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 
it through.

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 
> shorthand.
>
> 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 
> change.
>
> 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 
inside...

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 
steps.

>
> 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 
> ideas.

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.