D enters Tiobe top 20

[Timon Gehr]

On 12.11.19 05:25, Doc Andrew wrote:
> ...
> Other languages are pretty clear on the distinction between assumptions 
> and assertions. F* ("assume" - 
> https://www.riseforfun.com/FStar/tutorialcontent/guide#h24) & SPARK 
> ("pragma Assume" - 
> https://docs.adacore.com/spark2014-docs/html/ug/en/source/assertion_pragmas.html) 
> both make clear that assumptions are treated like axioms in their 
> provers, and must be used with caution. The Boogie IVL ("assume" - 
> http://chrisposkitt.com/files/teaching/SV-2015-AutoActiveVerification.pdf) 
> works the same way.
> ...

Yup.

> Coq has no "assume" keyword, but the "assumption" tactic takes a 
> hypothesis/premise and if it matches the goal (thing you're trying to 
> prove/assert), then it solves the goal).
> ...

Sure, it is shorthand for "there is an assumption that proves the goal". 
This is a completely standard usage.

> Frama-C/ANSI C Specification Language ("assumes" clause - 
> https://frama-c.com/download/acsl-1.14.pdf) just treats assumptions as 
> hypotheses/premises that imply some conclusion, so pre-conditions, as 
> far as I can tell. This might be where Walter is coming from in saying 
> that Asserts and Assumes would be the same in D.

It is not. Walter is arguing about run-time semantics and he uses some 
weird argument ("-release only removes the check, it doesn't remove the 
assumption") to justify the unsafe behavior of asserts with -release.

> This is the only 
> example I could find that uses "assume" like this, but there may be others.
> ...

The 'assumes' clause just says what assumptions are that the _function_ 
makes in order to satisfy the postcondition. It's saying "this function 
assumes ...", not "verifier, please assume ...". This is how 
preconditions operate. The function indeed assumes something, but it 
puts a burden on a caller who may not want to assume it.


> I think _most_ people consider Assert vs Assume the way SPARK and F* do 
> - as seen here: 
> https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 
> 
> 
> But hey, as Frama-C shows, it's not the only way to interpret those 
> keywords.

Frama-C shows no such thing. I'm not confused at all by an 'assumes' 
clause in a function signature that signifies a precondition.

> The English language gets in our way sometimes. Inflammable = 
> flammable, and all that.
> 
> If "assume" is taken to mean an "assert" which is a pre-condition,

Just to be clear: I have no problem at all with D's usage of 'assert' in 
preconditions. My point was that if you get rid of preconditions, 
'assert' cannot express preconditions, so the prover won't know whether 
the callee or the caller is responsible for discharging a certain assertion.

> then 
> fine, we could always point to Frama-C/ACSL to show that D isn't some 
> insane outlier and that we aren't a bunch of backwards idiots.

The -release flag turns asserts into optimizer assumptions. In -release 
mode, a failing assertion in @safe code is undefined behavior. (In the C 
sense.) Assume cannot be @safe, while assert can, but Walter conflates 
them into the same construct.

> It 
> wouldn't be the way _I_ would do it, but that's just one man's opinion, 
> and I'm biased by my use of SPARK where pragma Assume has a clear 
> meaning and works fine.
> 
> Given that we already have assert() in in{} contracts, to me the 
> assume() keyword (in Walter's reckoning of the meaning) is redundant, 
> and could be used for the axiomatic meaning.
> ...

Given that we have 'in' contracts, but we were arguing specifically 
about a scenario where we don't have them.

> If in{} and out{} contracts ever disappeared from the language, I think 
> an external solver would need something like assume()/require() to 
> distinguish preconditions from normal assertions.
> ...

Yes, this was exactly my point.