On Saturday, 13 June 2020 at 15:38:03 UTC, Johannes Pfau wrote:
> 
> To summarize and rephrase this: the encapsulation unit of @safe is the function boundary. The parameter definitions (including this pointer) and return type and their modifiers are the information the compiler uses to implement it's safety checks. For all possible combinations of these input values, the @safe function may not cause memory corruption.
>
> asserts then narrow the function contract by describing semantic limitations and @safe is not able to enforce this, as this information is not part of the function signature. This is fine, as @safe will still prevent soft UB from escalating to hard UB. But if you now use assert() as assume(), you introduce hard UB for some possible input combinations, subverting @safe guarantees.

Let me try and state the position I think you are taking.

Soft undefined behavior is unacceptable for @safe code because it can lead to memory corruption due to the hard undefined behavior which may result from the soft undefined behavior.

On 14.06.20 19:38, Jesse Phillips wrote:
> On Saturday, 13 June 2020 at 15:38:03 UTC, Johannes Pfau wrote:
>>
>> To summarize and rephrase this: the encapsulation unit of @safe is the function boundary. The parameter definitions (including this pointer) and return type and their modifiers are the information the compiler uses to implement it's safety checks. For all possible combinations of these input values, the @safe function may not cause memory corruption.
>>
>> asserts then narrow the function contract by describing semantic limitations and @safe is not able to enforce this, as this information is not part of the function signature. This is fine, as @safe will still prevent soft UB from escalating to hard UB. But if you now use assert() as assume(), you introduce hard UB for some possible input combinations, subverting @safe guarantees.
> 
> Let me try and state the position I think you are taking.
> 
> Soft undefined behavior is unacceptable for @safe code because it can lead to memory corruption due to the hard undefined behavior which may result from the soft undefined behavior.

No, soft undefined behavior is fine. The problem is that assert is explicitly specified to cause hard undefined behavior on failure, yet is allowed in @safe code.

On 14.06.20 17:14, Timon Gehr wrote:
> where each postcondition is established iff the corresponding precondition is established

Typo: That should have been `if`, not `iff`. (Of course the postcondition is allowed to hold even if the corresponding precondition does not.)

On Saturday, 13 June 2020 at 08:52:18 UTC, Johannes Pfau wrote:
> [snip]

A very good point, has not occured to me before. But I think I can give a more specific example of what you're trying to convey:

```
@safe auto readIndex(int[] arr, size_t i)
in (i < arr.length)
{	return arr[i];
}
```

Because the compiler is free to assume that the contract holds, it can elide the array bounds check. If it does that, it results in memory violation from `@safe` code.

This is something that should only be possible if `-boundscheck=off`. Not otherwise.

On Monday, 15 June 2020 at 04:08:28 UTC, Dukc wrote:
> On Saturday, 13 June 2020 at 08:52:18 UTC, Johannes Pfau wrote:
>> [snip]
>
> A very good point, has not occured to me before. But I think I can give a more specific example of what you're trying to convey:
>
> ```
> @safe auto readIndex(int[] arr, size_t i)
> in (i < arr.length)
> {	return arr[i];
> }
> ```
>
> Because the compiler is free to assume that the contract holds, it can elide the array bounds check. If it does that, it results in memory violation from `@safe` code.
>
> This is something that should only be possible if `-boundscheck=off`. Not otherwise.

Well, the compiler has an option specifically for in contracts, `-checkaction=in=[on|off]`, so probably what should be done is to give that option a `safeonly` value like what `-boundscheck` has.

On Monday, 15 June 2020 at 12:45:56 UTC, Paul Backus wrote:
>
> Well, the compiler has an option specifically for in contracts, `-checkaction=in=[on|off]`, so probably what should be done is to give that option a `safeonly` value like what `-boundscheck` has.

Typo: `-check=...`, not `-checkaction=...`.

On 15.06.20 14:45, Paul Backus wrote:
> On Monday, 15 June 2020 at 04:08:28 UTC, Dukc wrote:
>> On Saturday, 13 June 2020 at 08:52:18 UTC, Johannes Pfau wrote:
>>> [snip]
>>
>> A very good point, has not occured to me before. But I think I can give a more specific example of what you're trying to convey:
>>
>> ```
>> @safe auto readIndex(int[] arr, size_t i)
>> in (i < arr.length)
>> {    return arr[i];
>> }
>> ```
>>
>> Because the compiler is free to assume that the contract holds, it can elide the array bounds check. If it does that, it results in memory violation from `@safe` code.
>>
>> This is something that should only be possible if `-boundscheck=off`. Not otherwise.
> 
> Well, the compiler has an option specifically for in contracts, `-checkaction=in=[on|off]`, so probably what should be done is to give that option a `safeonly` value like what `-boundscheck` has.

One may want to disable assertion checking without potentially causing UB in @safe code. In fact, I think this is more common.

On Monday, 15 June 2020 at 12:45:56 UTC, Paul Backus wrote:
> Well, the compiler has an option specifically for in contracts, `-checkaction=in=[on|off]`, so probably what should be done is to give that option a `safeonly` value like what `-boundscheck` has.

This is not acceptable. The canonical way to use `assert`s is to assume they will not negatively affect the performance of the final build. Your proposal would break that assumption.

I personally see two options:
1: Simply disallowing the compiler for assuming that asserts hold.

2: Letting the compiler to assume most things like now, but disallow eliding array bound checks. In this case, there should also be a way for the user to add code that may not be elided by the optimizer, unless bounds checking is off. Something like:

```
@trusted auto readIndex(CustomIntArray arr, size_t i)
pragma(integritycheck, true) in (i < arr.length)
{	return arr[i];
}
```

Code with such a pragma could not be elided by trusting a regular assert (nor by trusting `enum` to have a valid value for example). It could still be elided by trusting another integrity critical assert, though.

On Saturday, 13 June 2020 at 08:52:18 UTC, Johannes Pfau wrote:

> A good article. Although there have sometimes been discussions about it, I think the difference between input validation and contract checking is now well understood by most people participating in discussions here.
>
> [...]

Looks like a fair and well-reasoned analysis.

On Saturday, 13 June 2020 at 03:46:38 UTC, Andrei Alexandrescu wrote:
> A short and sweet paper:
>
> http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1743r0.pdf
>
> It echoes Walter's opinions on contracts vs. runtime checking, to a tee. He has been derided on occasion in this group for such views. The paper is a good rationale from an independent source.

The approach trades security for performance. It can make sense, just should be opt in. I personally don't care what happens in release compilation mode, because my code doesn't rely on it, but many people were taught to use release mode, their code may not be ready for silent change of behavior.