DIP1028 - Rationale for accepting as is

[H. S. Teoh]

On Fri, May 22, 2020 at 05:26:03PM +0000, Adam D. Ruppe via Digitalmars-d-announce wrote:
[...]
> int snprintf(char[] buf, const char* fmt, ...) {
>    return c.snprintf(buf.ptr, buf.length, fmt, ...);
> }
> 
> Well, lol, that's not exactly *correct* thanks to the possibility of
> format string mismatch, but it bounds checks both sides of the slice
> and becomes more appropriately trusted due to the parameters being
> checked too.
> 
> We now actually have a trusted implementation with a safe interface -
> which is what @trusted is SUPPOSED to mean.

Ironically, it was Walter himself who was a staunch proponent of this.
And now we're basically saying, every C API is @safe by default unless
you take the pains to realize that, oh noes it takes a pointer and a
size and therefore passing the wrong size will cause buffer overflow
yikes we better mark it @system.  Seems totally backwards to me.

But anyway, thinking about this a little more, it occurs to me that what
we're trying to do here is really not 100% watertight @safe-ty, rather,
what we're trying to do here is to maximize the surface area of compiler
mechnical verification.  So @safe doesn't *really* mean "no memory
corruption, guaranteed", it means "compiler will do its best to verify
what it can, but what it can't, we just have to take on faith."  Or, to
put it more nicely, "this code is @safe modulo the safety of calls to
unverifiable C APIs".

Which leads to the idea of having some way of marking a function as
@safe up to the safety of {a delegate parameter, a C interface, etc.}. A
kind of conditional @safe-ty.  It has been a recurring need that keeps
coming up, e.g., in relation to the recent DIP on lazy parameters. For
example:

	// N.B.: hypothetical syntax
	int myFunc(int delegate(SomeObj obj) cb) @conditionalSafe {
		SomeObj obj = ...;
		// &obj++; // error: pointer arithmetic not allowed in @safe
		// systemFunc(); // error: cannot call systemFunc from @safe

		return cb(obj); // OK: we are @safe modulo safety of cb
	}
	void systemFunc() @system {...}

Then myFunc would become callable from @safe code, provided the
passed-in argument is also @safe.

The crucial point here is that while compiling myFunc, the compiler
doesn't (need to) know the @safe-ty of `cb`, it can just treat it as an
opaque object that it assumes the safety of, while it verifies the rest
of the function body.

This is parallel to C functions being of unverifiable safety, so if
extern(C) functions were somehow marked and treated as opaque objects of
unknown safety, then the compiler can still verify the rest of the code
and produce a certificate of safety (modulo the C APIs used).

If we had a way of expressing conditional safety, it could be a way to
salvage @safe from this current situation.


T

-- 
Doubtless it is a good thing to have an open mind, but a truly open mind should be open at both ends, like the food-pipe, with the capacity for excretion as well as absorption. -- Northrop Frye