On Saturday, 24 June 2017 at 05:16:45 UTC, MysticZach wrote:
> On Friday, 23 June 2017 at 21:36:07 UTC, Moritz Maxeiner wrote:
>> Contracts within the DbC paradigm *are* abstractions that do not necessitate any particular implementation.
>
> In practice, though, what must any such implementation actually achieve?
> [...]
> 2. prevent programs in invalid states from continuing

With "program" in this abtract domain meaning the specific computational task that broke the contract, not necessarily the entire implementation domain OS process - it's just that the finest safe termination of computational tasks in the presence of bugs on modern OSs you get for free (because of process isolation) is a process.
With a runtime environment (e.g. a VM like the JVM, or an appropriate druntime implementation) that supports safe killing on a finer resolution (e.g. threads and fibers) there's no inherent reason not to map contract violations to thread/fiber killing instead of process killing (if it's proven to be safe within that runtime).

> 3. provide information about those invalid states after the fact

All it *must* do is identify which contract failed (i.e. (file,line/row,column)). The rest is optional.

>> It would only couple the contracts with asserts if the DIP also specifies that asserts *must* be used for the lowering (which I would be against btw).
>
> [...]. I'd rather not deal with that problem. It's vastly easier to just put my faith into the `assert` grammar, and hope that any improvements that it needs and receives will apply equally to `assert`s as well.

I would simply copy the current assert grammar into a separate contract grammar, so that further modifications to the assert grammar do not change the new contract grammar.
But as I said, it's not important to me, it was just an observation/question. Should the need ever arise for (new) contract and assert grammar to diverge it can be dealt with then by whoever does the diverging.

On 6/24/17 8:26 AM, Moritz Maxeiner wrote:

> I would simply copy the current assert grammar into a separate contract grammar, so that further modifications to the assert grammar do not change the new contract grammar.
> But as I said, it's not important to me, it was just an observation/question. Should the need ever arise for (new) contract and assert grammar to diverge it can be dealt with then by whoever does the diverging.

Exactly, we can cross that bridge when (if) it happens.

-Steve

On Saturday, 24 June 2017 at 12:26:57 UTC, Moritz Maxeiner wrote:
> Should the need ever arise for (new) contract and assert grammar to diverge it can be dealt with then by whoever does the diverging.

Yes, I'll keep the grammar the same for now, because there is a benefit to doing so, in that any improvements to the assert grammar will immediately apply to the contract grammar too.

On Saturday, 24 June 2017 at 02:31:09 UTC, Solomon E wrote:
> I think my proposal to add another use of semicolon in parentheses, like `foreach` or `for` but not the same as either, was needlessly complicated.
>
> in (a)
> out (result) (a)
>
> as syntax sugar where each (a) lowers to
> {assert(a);}
> and in future can lower to something else, to renovate contract implementation
>
> That's so much easier, in every way.

Another option is to allow giving a name to a function's return value in its signature, so something like:

        int result myFunc(Args...)(Args args)
	if (Args.length > 1)
	in (args[0] > 0)
	out (result > 10);

This is the approach taken by Dafny, which was mentioned earlier in the thread. Can't say I like it.

On 6/23/17 6:52 PM, jmh530 wrote:
> On Friday, 23 June 2017 at 17:31:15 UTC, MysticZach wrote:
>>
>> OutExpression:
>>   out ( ; AssertParameters )
>>   out ( Identifier ; AssertParameters )
> 
> Why not?
> 
> OutExpression:
>    out ( AssertParameters )
>    out ( Identifier ; AssertParameters )

The path of least resistance is to use existing language constructs, i.e.

out result => assert(result > 0)


Andrei

On Sunday, 25 June 2017 at 11:37:07 UTC, Andrei Alexandrescu wrote:
> On 6/23/17 6:52 PM, jmh530 wrote:
>> On Friday, 23 June 2017 at 17:31:15 UTC, MysticZach wrote:
>>>
>>> OutExpression:
>>>   out ( ; AssertParameters )
>>>   out ( Identifier ; AssertParameters )
>> 
>> Why not?
>> 
>> OutExpression:
>>    out ( AssertParameters )
>>    out ( Identifier ; AssertParameters )
>
> The path of least resistance is to use existing language constructs, i.e.
>
> out result => assert(result > 0)

I consider adapting foreach syntax as using existing language constructs (instead of inventing completely new syntax).
And while your proposal may indeed be the path of least resistance (since you and Walter will end up deciding whether to accept it or not), it's also the path of least benefits as it still requires manually specifying the contract implementation. Coupling a contract with its implementation is verbose and can already be done with the existing syntax; imho it would ensure that the new syntax will receive only negligible more usage than the existing one.

On 25.06.2017 13:37, Andrei Alexandrescu wrote:
> On 6/23/17 6:52 PM, jmh530 wrote:
>> On Friday, 23 June 2017 at 17:31:15 UTC, MysticZach wrote:
>>>
>>> OutExpression:
>>>   out ( ; AssertParameters )
>>>   out ( Identifier ; AssertParameters )
>>
>> Why not?
>>
>> OutExpression:
>>    out ( AssertParameters )
>>    out ( Identifier ; AssertParameters )
> 
> The path of least resistance is to use existing language constructs, i.e.
> 
> out result => assert(result > 0)
> 
> 
> Andrei
This would face quite some resistance, on the following grounds:

out(result){ assert(result > 0); } // exists

out result => assert(result > 0) // more of the same

out(result; result > 0) // better

On Sunday, 25 June 2017 at 12:10:02 UTC, Timon Gehr wrote:
> On 25.06.2017 13:37, Andrei Alexandrescu wrote:
>> On 6/23/17 6:52 PM, jmh530 wrote:
>>> On Friday, 23 June 2017 at 17:31:15 UTC, MysticZach wrote:
>>>>
>>>> OutExpression:
>>>>   out ( ; AssertParameters )
>>>>   out ( Identifier ; AssertParameters )
>>>
>>> Why not?
>>>
>>> OutExpression:
>>>    out ( AssertParameters )
>>>    out ( Identifier ; AssertParameters )
>> 
>> The path of least resistance is to use existing language constructs, i.e.
>> 
>> out result => assert(result > 0)
>> 
>> 
>> Andrei
> This would face quite some resistance, on the following grounds:
>
> out(result){ assert(result > 0); } // exists
>
> out result => assert(result > 0) // more of the same
>
> out(result; result > 0) // better

out result => result > 0 // not much worse

out __result > 0 // even better (__result works at least since [0])

I suggested adding a shorter / better looking contextual keyword -
`result` - a while ago [1]:
---
out result > 0 // perhaps the best
---

And before that I proposed this:
---
// `Unqual` is not needed for `isNumeric` strictly speaking,
// it's used here only for illustration purposes.

T sqrt(T)(T n)
if Unqual!T U: isNumeric!U || is(U == BigInt)
in n >= 0
out (result) result * result == n
{
    //Implementation
}
---
(I think as a reply to you in the DIP1003 thread)


I'm wondering if `out result > 0` (or if not `out __result > 0`)
would be too much of a stretch for the language grammar.


[0]: https://github.com/dlang/dmd/commit/620acd53b63bfede6179a1b6a5c7d1b01a14ed0e#diff-1faebda3a5778a9d5b2dc0037a8f589bR8

[1]: https://github.com/dlang/DIPs/pull/66#discussion_r117613661

On Sunday, 25 June 2017 at 15:46:12 UTC, Petar Kirov [ZombineDev] wrote:
>
> out result => result > 0 // not much worse
>
> out __result > 0 // even better (__result works at least since [0])
>
> I suggested adding a shorter / better looking contextual keyword -
> `result` - a while ago [1]:
> ---
> out result > 0 // perhaps the best
> ---

I have no stance with having to specify a result identifier, or using __result, making `result` special, *but*: Not requiring parentheses here introduces an unacceptable language inconsistency:

auto x(T)(T t)
  if (...)
  in (...)
  out ...
{
    ...
}

If you also propose to drop the parentheses for `in`, that still leaves the inconsistency with `if`, i.e. now `if` must be changed to also drop the parentheses in template constraints. That, however, leads then to an inconsistency between different uses of `if` and thus all other occurrences of `if` in the grammar must now be made to work without parenthesis. This then leads to even more inconsistencies with `for`, `while`, etc. that now also will have to be changed.

>
> I'm wondering if `out result > 0` (or if not `out __result > 0`)
> would be too much of a stretch for the language grammar.
>

As argued above, it would essentially require making all uses of parenthesis for conditions optional or introduce atrocious inconsistencies.
If this is to be done, I believe it belongs in a separate DIP "Optional parenthesis for conditions", while this DIP uses parentheses.

On Sunday, 25 June 2017 at 15:46:12 UTC, Petar Kirov [ZombineDev] wrote:
> out result > 0 // perhaps the best

How would you handle things like this:

T minimum(T)(RedBlackTree!T tree)
in (!tree.empty)
out result in (tree)
{
    return tree.front;
}

That could either mean "out(result){assert(result in (tree));}" or out(result){assert(result);} in{assert(tree);}"