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.
