RFC: scope and borrowing

[via Digitalmars-d]

On Monday, 25 August 2014 at 15:38:09 UTC, Ola Fosheim Grøstad 
wrote:
> On Monday, 25 August 2014 at 11:09:48 UTC, Marc Schütz wrote:
>> I believe this proposal is close to the best we can achieve 
>> without resorting to data flow analysis.
>
> I agree with bearophile, perhaps data flow analysis would be 
> desirable. So I think it would be a good idea to hold the door 
> open on that.

I definitely don't want to exclude anything. But we need to find 
out whether the additional complexity of full-blown DFA is really 
necessary, see my reply to bearophile.

>
>> I'm unfortunately not familiar with the theoretical 
>> foundations of type systems, and formal logic. So I'm not sure 
>> what exactly
>
> I don't know all that much about linear type systems, but this 
> is an opportunity to learn more for all of us! :-)
>
>> you mean here. It seems to me the problems with @safe are with 
>> the way it was implemented (allow everything _except_ certain 
>> things that are known to be bad, instead of the opposite way: 
>> allow nothing at first, but lift restrictions where it's safe 
>> to do so), they are not conceptual.
>
> Because real programming languages are hard to reason about it 
> is difficult to say where things break down. So one usually 
> will map the constructs of the language onto something simpler 
> and more homogeneous that is easier to reason about.
>
> When it comes to @safe I think the main problem is that D makes 
> decisions on constructs and not on the "final semantics" of the 
> program. If you have a dedicated high level IR you can accept 
> any program segment that can be proven to be memory safe in 
> terms of the IR. The point is to have an IR that is less 
> complicated than the full language, but that retains needed 
> information that is lost in a low level IR and which you need 
> to prove memory safety.
>
> memset() is not unsafe per se, it is unsafe with the wrong 
> parameters. So you have to prove that the parameters are in the 
> safe region. Same thing with freeing memory and borrowed 
> pointers etc. You need a correctness proof even if you give up 
> on generality.
>
> You may reject many safe programs but at least verify as many 
> simple safe programs as you can.
>
> A bonus of having a high level IR is that you more easily can 
> combine languages with fewer interfacing problems. That would 
> be an advantage if you want a DSL to cooperate with D.

But this would require knowledge about the inner workings of 
memset() to be part of the IR, or memset() to be implemented in 
it. The same IR (or an equivalent one) would then need to be part 
of language specification, otherwise different compilers would 
allow different operations.

IMO the general idea of the current design is not okay, because 
it's easy to implement, and easy to specify (a whitelist, or as 
currently, blacklist approach). If something has been overlooked, 
it can be added incrementally; at the same time there's always 
@trusted to let the programmer specify what the compiler can't 
prove.