Here is a set of examples of annotated programs that have been formally proved correct for those interested:

http://toccata.lri.fr/gallery/why3.en.html

The advantage of formally separating what is proven from what is to be proved is quite obvious. You can generate annotated bindings for libraries and frameworks that can both increase correctness and provide semantic information that can be relied on (for optimization and other purposes).

On 7/30/2014 2:12 AM, bearophile wrote:
>> The optimizer can certainly use asserts to provide semantic information (even
>> though the dmd one doesn't at the moment).
>
> This is not a good idea. That's the job for assume(), not for assert.

The two are without distinction.


> In general assert() verifies something is true, and if it's false, the program
> just raises an assert error, that is even recoverable.

No, it is not recoverable.


> assert() can be used freely in your code, to make sure you have not done a
> mistake. assume() is only for special situations where you know something is
> true, that the compiler can't prove by itself.

Again, everything you say is true for assume is true for assert, and vice versa.

On 7/30/2014 5:52 AM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Wednesday, 30 July 2014 at 09:12:56 UTC, bearophile wrote:
>> And assume() and assert() are two different things, used for different
>> purposes. Do not give the same name to two so different features, if you want
>> to keep a language sane.
>
> Exactly. If you want to establish that the provided input is never zero and that
> the program doesn't need to be correct in that case, you do this:
>
> assume(input!=0);
>
> If you want to specify that the input should be prevented from being zero, you
> do this:
>
> if(input!=0){
>    assert(input!=0);
> }

Now you're trying to use assert to validate user input. This is a terrible, terrible misunderstanding of assert.

On 7/30/2014 2:12 AM, bearophile wrote:
> Info about assume in Microsoft C++:
> http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx

Note that document shows how assert is implemented using assume. I.e. they are the same thing.

Intriguingly, the __assume(0) behavior is even special cased like D's assert(0). C++ continues to adopt D features :-)

On Wednesday, 30 July 2014 at 20:33:41 UTC, Walter Bright wrote:
>> assume(input!=0);
>>
>> If you want to specify that the input should be prevented from being zero, you
>> do this:
>>
>> if(input!=0){
>>   assert(input!=0);
>> }
>
> Now you're trying to use assert to validate user input. This is a terrible, terrible misunderstanding of assert.

Can you please read the Hoare article form 1969? This is getting really annoying.

I am not trying to use assert to validate user input. I am verifying that the program is in compliance with the specification. Basically doing a partial proof of the theorem in the assert on the fly.

Example 1:

assume(x!=0) // define an axiom "x!=0"

Example 2:
if(x!=0){
   assert(x!=0) // prove theorem "x!=0" (successful)
}

Example 3:

assert(x!=0) // prove theorem "x!=0" (failure)

Example 4:

assume(x!=0); // define "x!=0" (impose constraint)
assert(x!=0); // prove theorem "x!=0" (successful)

I can't do better than this! Think of assume() as preconditions and assert() as postconditions.

Note also that you could use an existing theorem prover to prove a function correct, then machine translate it into D code with assume() and assert() and other machinery needed for provable correct programming in D.

Don't dismiss the distinction without thinking about it. Read Hoare's article, it is pretty well written.

On 7/30/2014 7:36 AM, Ary Borenszweig wrote:
> Now, if you compile in release mode, according to Walter, all the "asserts" are
> gone (which, as a side note, is something I don't like: in every case it should
> throw an AssertError). So the question is: can the compiler still replace that
> writeln call?

Yes.

On 7/30/14, 11:31 AM, Timon Gehr wrote:
> On 07/30/2014 07:56 PM, Andrei Alexandrescu wrote:
>> On 7/30/14, 9:31 AM, Timon Gehr wrote:
>>> 'lazy', which denotes pass by name instead of pass by need.
>>
>> It's not pass by name.
>> ...
>
> How so? Is it about failure to allocate a closure?

void fun(lazy int a) { ... }
int x = 42;
fun(x + 2);

"x + 2" doesn't have a name.

>>> 'pure' which denies access to mutable static variables and IO.
>>
>> That's the consequence of functional purity as defined by D.
>
> Somewhat debatable, but unworthy of debate.

Then don't mention it.

>> Consider this: after considerable effort you are failing to explain your
>> case for "assume" to the language creators.
>
> I think there was no such case (yet), only an unsuccessful attempt to
> clear up a misunderstanding based on terminology.

My perception is you were arguing for a very subtle distinction, one that would hardly deserve a language feature.

>> How do you think you'll fare with newcomers?
>> ...
>
> Hopefully, awesomely. Much less preconceptions.

May you have less snarky users than I do :o).


Andrei

On Wednesday, 30 July 2014 at 09:11:31 UTC, Walter Bright wrote:
> On 7/30/2014 12:54 AM, David Bregman wrote:
>> On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
>>> I don't either. I still have no idea what the difference between assume(i<6)
>>> and assert(i<6) is supposed to be.
>>
>> assert:
>> is a runtime check of the condition.
>> is a debugging/correctness checking feature.
>> is used when the expression is believed true, but is not proven so.
>> (if it was proven, then there is no purpose in asserting it with a redundant
>> runtime check that is guaranteed to never activate.)
>>
>> assume:
>> passes a hint to the optimizer to allow better code generation.
>> is used when the expression is proven to be true (by the programmer, like
>> @trusted).
>
> It still means the same thing as assert.
>
>
>> The only relation between the two is that if a runtime check for (x) is inserted
>> at some point, it is safe to insert an assume(x) statement afterwards, because x
>> is known true at that point.
>
> I.e. they're the same thing.
>
>
>> If assert degenerates to assume in release mode, any bugs in the program could
>> potentially cause a lot more brittleness and unexpected/undefined behavior than
>> they otherwise would have. In particular, code generation based on invalid
>> assumptions could be memory unsafe.
>
> Which is why assert can also do a runtime check.

I think you misread, none of that follows from what I wrote. Also, "Nuh-uh, they are too the same" is not a valid argument.

Can you please address the fact that assume is not @safe? How do you propose to preserve memory safety in release mode if you remove runtime checks for asserts but still assume the condition for codegen?

Ola Fosheim Grøstad:

> Here is a set of examples of annotated programs that have been formally proved correct for those interested:
>
> http://toccata.lri.fr/gallery/why3.en.html

I have started to read those pages, it looks interesting. From one of the first links (Sudoku solver):


valid values are 0..9. 0 denotes an empty cell

  predicate valid_values (g:grid) =
    forall i. is_index i -> 0 <= g[i] <= 9


So can't they represent that the value 0 is an empty cell in the code instead of comments? (I think this is possible in Ada language).

It's a bit sad that D1 has removed the literate programming feature of D1. In Haskell it's used all the time.

Bye,
bearophile

On Wednesday, 30 July 2014 at 20:47:30 UTC, Walter Bright wrote:
> On 7/30/2014 7:36 AM, Ary Borenszweig wrote:
>> Now, if you compile in release mode, according to Walter, all the "asserts" are
>> gone (which, as a side note, is something I don't like: in every case it should
>> throw an AssertError). So the question is: can the compiler still replace that
>> writeln call?
>
> Yes.

This on the other hand is a terrible, terrible misuse of assert.

You need distinguish between what is assumed to hold and what is proved to hold to chain together pieces of proven programs. So what one function require (preconditions) you need to assert before calling the function. On the other hand, what the function asserts you can assume to hold after the call.

So:

assert(X)
---- function call to precompiled library code
assume(X)
...statements
assert(Y)
---- function return from precompiled library code
assume(Y)


Pretty clear, now huh?