safety: null checks

[Paul Backus]

On Monday, 23 November 2020 at 00:50:03 UTC, Ola Fosheim Grostad 
wrote:
> On Monday, 23 November 2020 at 00:33:35 UTC, Paul Backus wrote:
>>
>> @safe code is allowed to dereference pointers, and there's no 
>> way for the compiler to know at compile time which pointers 
>> are null and which aren't. So, either @safe code must be 
>> forbidden from creating null pointers in the first place, or 
>> it must be allowed to dereference them.
>>
>> Remember, @safe doesn't just mean "code that's memory safe", 
>> it means "code that the compiler can *prove* is memory safe."
>
> Well, the spec said that the value should be valid, which null 
> by definition should not have,

Please show me the definition of null that requires it to be 
invalid.

> then the example comment mentioned a well defined crash which 
> is a contradiction in terms.
>
> So the spec is unsound.

Please show me the relevant definitions of these terms and 
explain how they contradict.

> What you would require from a high level language is that 
> dereferencing null pointers is caught either at compile time or 
> at runtime. But that is slow on some platforms. So this is just 
> an example of the implementation being the spec, and actual 
> document does not make sense in a general setting.

The implementation allows undefined behavior in @safe code. That 
means the implementation is incorrect, period. Neither of the 
possible interpretations of the spec allow this.