Simplification of @trusted
Paul Backus
snarwin at gmail.com
Thu Jun 17 22:03:47 UTC 2021
On Thursday, 17 June 2021 at 21:16:02 UTC, ag0aep6g wrote:
> On Thursday, 17 June 2021 at 21:00:13 UTC, Paul Backus wrote:
>> On Thursday, 17 June 2021 at 20:42:20 UTC, Ola Fosheim Grøstad
>> wrote:
>>> On Thursday, 17 June 2021 at 20:33:33 UTC, Paul Backus wrote:
>>>> Assuming [issue 20941][1] is fixed, yes.
>>>
>>> […]
>>>
>>>> Yes.
> [...]
>> The interpretation that I and ag0aep6g have been describing is
>> the correct one.
>
> Yet I would answer "no" where you answered "yes" above.
>
> The question was: "Yes, but if I make size() @trusted and fix
> the bug then interface is provably safe?".
>
> The corresponding code:
>
[...]
>
> In my opinion, that code is fundamentally equivalent to this
> (regarding the safety of `get`):
>
> ```d
> int get(int* ptr, int offset) @trusted { return ptr[offset]; }
> ```
> That function does not have a safe interface, because it
> exhibits undefined behavior wenn called like `get(new int,
> 1000)`, which @safe code can do.
In current D, yes, because issue 20941 means that `private`
cannot be relied upon for encapsulation--thus the caveat.
However, if we assume for the sake for argument that @safe code
*can't* bypass `private`, then it is possible to prove that the
invariant `offset < 2` is maintained by examining only code in
the module where `offset` is defined. And once we've proven that
invariant, we can prove that `get` is always memory safe when
called from `@safe` code.
I will grant that, even in this hypothetical, `get` still would
not satisfy the definition of "safe interface" currently given in
the language spec--but at that point, who cares? The current
definition is valid for the current language, but if the language
changes, the definition ought to be updated too.
More information about the Digitalmars-d
mailing list