D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Saturday, 9 November 2019 at 21:11:14 UTC, Doc Andrew wrote:
> I'm pretty ignorant of how all that would all work, is there 
> some sort of a standard way to give optimizers "hints" based on 
> what the solver can show?

I don't think so, but if you establish something that is to weak 
for verification it still can potentially be used for 
optimization.


> I don't want to over-sell the potential performance gains.

Of course not, you would have to provide actual examples.  The 
"easy" gains would be from removing dynamic checks, but not so 
easy in reality.  If it is easy then the optimizer can already do 
it using dataflow analysis.

So figuring out "trivial" small examples where the optimizer 
fails by looking at generated assembly is a good starting point.


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


> (Longer-term, consider a change to the language to create a 
> foreach expression or add a new expression "forall" (or 
> something). I would anticipate a lot of weeping and gnashing of 
> teeth.)

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.


> - Loop invariants: Allow invariant{} blocks inside loop 
> statements in addition to classes and structs. This is the only 
> part of the DIP that I can foresee requiring a language change; 
> I don't know any way of attaching a UDA to a statement. I 
> _think_ this would be the only blocker.

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.

> (Even better would be strong subtypes, refinement types, or 
> first-order types, but you can simulate them well enough with 
> contracts in an invariant clause).

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

> A smaller language change would be to give invariant a 
> parameter with a hypothetical or ghost variable and allow it on 
> aliases:

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?

> I'd welcome any more-informed thoughts on how to proceed and go 
> through the DIP process, if there's interest!

I don't know enough about what makes a DIP succeed.  What is 
common in other languages is to make a library/tool 
implementation first as  proof of concept and then argue that it 
would be better as a language extension.

So that probably is the better approach... But I don't know.

But reserving the vocabulary makes a lot of sense. Then I would 
point to other languages, particularly FV languages, so that you 
reserve the most common terms "@requires", "@ensures", "@forall", 
"@exists" etc.

But in a proof-of-concept you can just use "_vc_requires" or some 
other prefix.

>> I am actually not sure how this could be done well. Because 
>> you could have array accesses within a conditional expression.
>
> Flow analysis can sort that out, checking both branches of the 
> conditional and making sure that contracts hold in every case.

No, I meant how to express it syntactically in a way that allows 
you to distribute pre-verified code.

(The point of having verification would be to cover those cases 
that standard flow analysis fail on.)

> analysis. The first time you see warnings like "Cannot prove 
> abc is less than def (example: def = 255)" because you didn't 
> consider edge cases, it opens your eyes to how proofs can 
> really save you from a lot of testing and debugging.

Yes, maybe that is a use case.

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.


> One kind of neat thing that SPARK has is the ability to break 
> volatile down into sub-categories like "Effective_Reads", where 
> reading a value takes something off a UART, or 
> "Effective_Writes", where writing to a hardware register has 
> some effect on the system, and "Async_Readers/Writers" where 
> some hardware will be accessing memory behind the scenes... now 
> how that affects the state of a proof, I'm not totally sure.

IIRC, D does not provide volatile though... You have to use 
something intrinsics-like. So memory mapped registers are not 
types in D, it is dealt with as a memory fenced access-action...


> So, having done no DMD compiler hacking myself, is the state of 
> the "DMD as a library" mature enough now to where somebody 
> could import dmd.compiler, get an AST and start figuring out 
> VCs?

No idea. I think the major hurdle for you would be the templating.

Maybe only deal with non-templated code, because then you can use 
one of the D parsers and rewrite the code with 
verification-annotations instead of modifying the actual 
compiler. For a proof-of-concept.


> A DIP without some sort of prototype tooling, even if 
> primitive, is going to be pretty toothless, IMO.

Yes. You could write something "informational". Then evolve it 
later.

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.