D enters Tiobe top 20

[Doc Andrew]

On Sunday, 10 November 2019 at 10:22:27 UTC, Timon Gehr wrote:
> - Modular verification means it's enough to have DI files for 
> functions you call, without a function body.
>
In a unit testing world, every assert gets checked every time the 
function is called anyhow, so it makes little difference whether 
they are pre or post-conditions, or just sprinkled throughout a 
function.

In a verified world, it makes a _huge_ difference. A verified 
function with an "in" contract states, "this function satisfies 
all of its contracts (explicit and implicit) _if and only if_ the 
in contracts/preconditions are satisfied".

With this, once that function is verified,
a caller need only make sure that it satisfies those 
preconditions at each call site. In the absence of preconditions, 
the verifier has to re-prove _every_ assert() in the callee 
function (and every OTHER function that the callee uses too...) 
_every time_ it's called throughout the program. It's an 
exponential increase in the problem space.

You _might_ be able to do a flow analysis to suss out which 
asserts are considered preconditions without explicitly stating 
so, but it seems like a tough problem, and explicitly stating 
them seems like a better practice anyhow.

Modular verification is really the only tractable way to approach 
the problem. You build up the proof starting from leaf functions 
which, once proven, need only their pre-conditions checked at 
subsequent calls. Globals and functions with side-effects 
complicate this somewhat, but for pure functions it works very 
cleanly.

And like Timon said, in the absence of in/ out contracts in a .di 
file, verified libraries provide no way to extend their 
guarantees to the user.

-Doc