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
):
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.