D enters Tiobe top 20

[Doc Andrew]

On Monday, 11 November 2019 at 22:30:18 UTC, Timon Gehr wrote:
> On 11.11.19 11:39, Walter Bright wrote:
>> 
>> The distinction between assert and assume has come up before, 
>> and I've argued that in D they are the same.
>
> Which I have argued is complete insanity. I'm getting pretty 
> angry here. Not sure what to do about it.

I'd expect a FV DIP to hash this out and get everybody on the 
same page. Different languages, different textbooks, different 
mathematicians all use slightly different vocabularies for this 
stuff, so it can get confusing.

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.

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

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. This is the only example I could find that uses 
"assume" like this, but there may be others.

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

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.

Having said all that, we probably need to use a little more 
mathematical rigor with how we define these regardless of the 
words we choose to describe the concepts.

It would also mean we'd need another keyword/UDA to use for an 
axiom, like, uh, @axiom. But then we're getting into weird math 
terms that scare people off. So that's probably why "assume" is 
preferred by some of the others.

-Doc