@trusted assumptions about @safe code

[Paul Backus]

On Wednesday, 27 May 2020 at 17:02:15 UTC, ag0aep6g wrote:
> I'm not sure where you stand on this: If an @safe function is 
> documented to return 42, can we rely on that in the same way we 
> can rely on strlen's documented behavior? Let's say that the 
> author of the @safe is as trustworthy as the C standard library.

It depends entirely on how far you are willing to extend your 
trust. If you're willing to trust the C library to conform to the 
C standard, and you stipulate that this other function and its 
documentation are equally trustworthy, then yes, you can trust it 
to return 42.

I think the key insight here is that the memory-safety property 
established by D's @safe is *conditional*, not absolute. In other 
words, the D compiler (modulo bugs) establishes the following 
logical implication:

     my @trusted code is memory-safe -> my @safe code is 
memory-safe

Proving the left-hand side is left as an exercise to the 
programmer.

In practice, proving your @trusted code correct without making 
*any* assumptions about other code is too difficult, since at the 
very least you have to account for dependencies like the C 
library and the operating system. At some point, you have to 
trust that the code you're calling does what it says it does. So 
what you end up doing is establishing another logical implication:

     my dependencies behave as-documented -> my @trusted code is 
memory-safe

By the rules of logical inference, it follows that

     my dependencies behave as-documented -> my @safe code is 
correct

This is far from an absolute safety guarantee, but it can be good 
enough, as long as you stick to dependencies that are 
well-documented and well-tested.

Of course, if you are willing to put in enough effort, you can 
tighten up the condition on the left as much as you want. For 
example, maybe you decide to only trust the C library and the 
operating system, and audit every other dependency yourself. Then 
you end up with

     my libc and OS behave as-documented -> my @safe code is 
correct

This is more or less the broadest assurance of safety you can 
achieve if you are trying to write "portable" code, and I expect 
the vast majority of programmers would be satisfied with it.

In princple, if you are doing bare-metal development, you could 
get all the way to

    my hardware behaves as-documented -> my @safe code is correct

...but that's unlikely to be worth the effort outside of very 
specialized and safety-critical fields.