RFC: scope and borrowing

[via Digitalmars-d]

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'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 if you see potential problems, or know a way to avoid them, 
> this is exactly the kind of thing I'd like to see discussed.

The problem is that D is too complex to reason about with any 
reasonable level of confidence. So you need to reduce the 
language to a level where you can reason about it with confidence 
and build the other constructs on top of that.

(That way you don't have to reason about the combinatorial 
explosion of constructs, just the building blocks).

Ola.