D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Saturday, 9 November 2019 at 02:55:37 UTC, Doc Andrew wrote:
> It could be done in baby steps, too - maybe start with a tool 
> that just shows no bad behavior occurs in a simple expression.

Exactly right.

PREREQUISITE:

Add something like «assume» to the language and make the 
optimizer add those to its fact database. For LLVM this should be 
trivial.

Then add «assume» clauses to the standard library that are 
manually proven correct and also add an option to convert assume 
to assert for additional unit-testing. This allows you to get 
started working on the optimizer and figure out how to make good 
use of the extra facts.

Also, optimizing the standard library affects all compiled 
programs... so even small gains might be worthwhile.


STAGE 2:

Add ensure-statements to the language. Those will be converted to 
assume-statements if you throw a switch, but display a warning 
that all ensure-statements have to be proven correct by an 
external verifier before compilation. Thus the entire burden has 
been moved to an external tool.

This would encourage third parties to work on tools to translate 
D code into verifiable code to be consumed by standard 
verification tooling.

Extension: create an online certification service that allows 
library code to carry a certificate that the library code has 
been verified. So that all their ensure statements can be turned 
into assume without throwing a switch. Certificates can be 
revoked (in case you find a bug in the verification process).


STAGE 3:

Then break all dynamic checks out as asserts by transforming the 
code. So that all bounds checks turn up as asserts. Break 
composite asserts into individual asserts.

Verifying individual functions:
step 1.1: use data-flow to convert as many asserts as possible 
into assumes
step 1.2: use an external verifier to prove others if possible

If those fail, try to do the verification at the call site:
step 2.1: create a unique copy of the function for the call site
step 2.2: use dataflow to bring additional assumed preconditions 
into the called function
step 2.3: go to step 1.1

> Then show the same for entire @pure functions. From there 
> someone could work up to proving that pre/post-conditions in 
> @pure functions are satisfied. Then maybe go on to do 
> invariants, then work up to @safe @nogc code, and so on.

Yup, start with the easy ones. Like pure functions provided as 
parameters to functions that work on arrays which often. Could 
even limit it to the ones used in the standard library.