On 06/18/14 10:14, Walter Bright via Digitalmars-d wrote:
> 
> Also, D is a collaborative effort. If there's an issue that engages your interest, step up and help out. I simply cannot do everything. This n.g. is full of "you should do this, you should do that" largely directed at me. You guys want things to happen, make them happen!

And most of those requests completely ignore language context, are indiscriminately trying to copy or transplant other concepts, or give a suboptimal answer to the wrong question. It's frustrating to even just read them; I have several times considered unsubscribing, as watching things go in a wrong and very unproductive direction isn't fun.

The one thing that /you/ could do, which would make the most difference, is splitting up the compiler into a free frontend [1] and the non-free "rest". The current situation results in people avoiding looking at or even going near DMD at all. The number of potential contributors is already low enough, and the fuzzy licensing situation drives away the most valuable ones (since those will often be the ones which treat the legal aspects seriously and the risks involved when dealing with this kind of mixed free and proprietary code within one repo are too high).

(JIC someone suggests working on the frontend via LDC/GDC trees - that would inevitably result in a language fork eventually.)

artur

[1] the many problems with the artistic license are now gone, after the
    switch to boost; at least the license itself is no longer an issue.

On Wednesday, 18 June 2014 at 08:13:59 UTC, Walter Bright wrote:
> On 6/18/2014 12:05 AM, deadalnix wrote:
>> On Wednesday, 18 June 2014 at 07:02:43 UTC, Walter Bright wrote:
>>> On 6/17/2014 11:50 PM, deadalnix wrote:
>>>> and the fact that @safe is defined backward (ie by listing what is not
>>>> allowed and
>>>> adding to the list when new holes are discovered
>>>
>>> https://issues.dlang.org/buglist.cgi?bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&keywords=safe%2C%20&keywords_type=allwords&list_id=41168&query_format=advanced
>>>
>>>
>>> Currently, there are zero bugzilla issues tagged with 'safe'. Please file
>>> bugzilla issues for which ones are discovered and tag them!
>>
>> I don't even know what to answer to that. We are clearly talking past each other
>> here, and I have no idea how to convey the message in a better way.
>
> 1. A long list of problems with @safe has been asserted, but I have not been able to elicit any enumeration of them, so the extent of this problem is completely unknown.
>
> 2. The definition of @safe in the spec is asserted to be utterly wrong, but no corrected definition has been proposed.
>
> 3. A new approach to designing @safe has been proposed in vague terms, but nothing specific and no offers of help to flesh it out.
>
>
> From my perspective, it is like bug reports I'd often get for the compiler that consisted solely of:
>
>     "Your compiler doesn't work."
>
> It's just not helpful. There's nothing I can do with that.
>
> Also, D is a collaborative effort. If there's an issue that engages your interest, step up and help out. I simply cannot do everything. This n.g. is full of "you should do this, you should do that" largely directed at me. You guys want things to happen, make them happen!

You two speak different languages here, I'll try to translate:

Basically deadalnix argues that memory safety cannot be checked by a machine (there's a proof for that) and as @safe-ness can be checked it obviously is not equivalent to memory safety. Further *any* definition of @safe-ness that can be expressed by a finite set of mathematical rules will not be equivalent to memory safety.

Then the big misunderstanding is the "equivalence". Equivalence means that
  1) @safe implies memory-safe
  2) !@safe implies !memory-safe

Clearly Walter is only talking about 1), and there is no reason why you couldn't have a @safe-ness check that implies memory-safety. It just won't be *equivalent*.

On Wednesday, 18 June 2014 at 06:35:01 UTC, Ola Fosheim Grøstad
wrote:
> Not really, you can prove termination for all programs with 3 instructions and 3 bytes of RAM. You can do it for all programs with 4 instructions and 4 bytes of RAM. You can do it for all programs with N instructions and N bytes of RAM. You cannot do it for all TMs since they have unbounded storage.
>
> Thus you can prove non-trivial properties such as whether a functions returns with 1, whether it accepts or rejects the input '0', etc. It might take a lot of time, but you can do it in a fixed amount of time. You cannot do it for TMs.

Maybe I missed something in this discussion, but unless you are
not including jumps/loops in those N instructions, just because
the number of instructions and memory is bounded does not mean
you can prove (for arbitrary programs) that the program
terminates.

I hope I don't shoot myself in the foot by trying to come up with
a concrete example, but let me try. Consider the program to
calculate whether some point is part of the Mandelbrot set. The
program only requires a small and fixed amount of memory but for
some points it may iterate forever (practical fractal programs
set an iteration limit, but let's assume this one doesn't, for
the sake of the argument).

On Wednesday, 18 June 2014 at 07:05:13 UTC, deadalnix wrote:
> On Wednesday, 18 June 2014 at 07:02:43 UTC, Walter Bright wrote:
>> On 6/17/2014 11:50 PM, deadalnix wrote:
>>> and the fact that @safe is defined backward (ie by listing what is not allowed and
>>> adding to the list when new holes are discovered
>>
>> https://issues.dlang.org/buglist.cgi?bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&keywords=safe%2C%20&keywords_type=allwords&list_id=41168&query_format=advanced
>>
>> Currently, there are zero bugzilla issues tagged with 'safe'. Please file bugzilla issues for which ones are discovered and tag them!
>
> I don't even know what to answer to that. We are clearly talking past each other here, and I have no idea how to convey the message in a better way.

Create a bugzilla issue to make everything unsafe and list there constructs you think can be defined as safe :)

On Wednesday, 18 June 2014 at 11:09:14 UTC, Artur Skawina via Digitalmars-d wrote:
> The number of potential contributors is
> already low enough, and the fuzzy licensing situation drives away the
> most valuable ones (since those will often be the ones which treat the
> legal aspects seriously and the risks involved when dealing with this
> kind of mixed free and proprietary code within one repo are too high).

Wait what? Do you know a single person who decided to not work on DMD FE because of kind of formally (but not practically) non-free backend?

On Wed, Jun 18, 2014 at 04:39:27PM +0000, Dicebot via Digitalmars-d wrote:
> On Wednesday, 18 June 2014 at 07:05:13 UTC, deadalnix wrote:
> >On Wednesday, 18 June 2014 at 07:02:43 UTC, Walter Bright wrote:
> >>On 6/17/2014 11:50 PM, deadalnix wrote:
> >>>and the fact that @safe is defined backward (ie by listing what is not
> >>>allowed and
> >>>adding to the list when new holes are discovered
> >>
> >>https://issues.dlang.org/buglist.cgi?bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&keywords=safe%2C%20&keywords_type=allwords&list_id=41168&query_format=advanced
> >>
> >>Currently, there are zero bugzilla issues tagged with 'safe'. Please file bugzilla issues for which ones are discovered and tag them!
> >
> >I don't even know what to answer to that. We are clearly talking past each other here, and I have no idea how to convey the message in a better way.
> 
> Create a bugzilla issue to make everything unsafe and list there constructs you think can be defined as safe :)

Everyone talks about it, but nobody does anything about it, so here goes nothing:

	https://issues.dlang.org/show_bug.cgi?id=12941

Obviously, I have no idea what should go in that list, so everyone who cares about this issue, please chime in. Thanks!

P.S. I've also tagged a whole bunch of issues with 'safe'. It's just based on a quick skim over all issues that turned up when I searched for 'safe', so I may have mistagged some, and missed others, but this is just to get the ball rolling. Please fix wrong/missing tags if you find them. :)


T

-- 
I'm still trying to find a pun for "punishment"...

On Wednesday, 18 June 2014 at 15:25:11 UTC, Luís Marques wrote:
> On Wednesday, 18 June 2014 at 06:35:01 UTC, Ola Fosheim Grøstad
> wrote:
>> Not really, you can prove termination for all programs with 3 instructions and 3 bytes of RAM. You can do it for all programs with 4 instructions and 4 bytes of RAM. You can do it for all programs with N instructions and N bytes of RAM. You cannot do it for all TMs since they have unbounded storage.
>>
>> Thus you can prove non-trivial properties such as whether a functions returns with 1, whether it accepts or rejects the input '0', etc. It might take a lot of time, but you can do it in a fixed amount of time. You cannot do it for TMs.
>
> Maybe I missed something in this discussion, but unless you are
> not including jumps/loops in those N instructions, just because
> the number of instructions and memory is bounded does not mean
> you can prove (for arbitrary programs) that the program
> terminates.
>

Jumps and loops don't matter. The point is that such a program only has a finite amount of possible states: The 4 bytes of RAM, plus the current instruction pointer (to be 2 bits for 4 instructions). In this case, there are only

    2^(4*8) * 2^2 = 2^34 = 17179869184

different states. If during execution you encounter a state that you've already seen before, you know that the program will go into an infinite loop. This is easy to implement using a bitmap.

Of course, said bitmap will soon become too large to handle in practice if you want to analyze realistic "interesting" programs.

On Wednesday, 18 June 2014 at 19:17:50 UTC, Marc Schütz wrote:
> Jumps and loops don't matter. The point is that such a program only has a finite amount of possible states: The 4 bytes of RAM, plus the current instruction pointer (to be 2 bits for 4 instructions). In this case, there are only
>
>     2^(4*8) * 2^2 = 2^34 = 17179869184
>
> different states. If during execution you encounter a state that you've already seen before, you know that the program will go into an infinite loop. This is easy to implement using a bitmap.
>
> Of course, said bitmap will soon become too large to handle in practice if you want to analyze realistic "interesting" programs.

Ah, right, my bad :-)

On Wednesday, 18 June 2014 at 15:25:11 UTC, Luís Marques wrote:
> Maybe I missed something in this discussion, but unless you are
> not including jumps/loops in those N instructions, just because
> the number of instructions and memory is bounded does not mean
> you can prove (for arbitrary programs) that the program
> terminates.

Yes, you can. You just run it until it enters a previous state. At that point you have an infinite loop and it won't terminate.

Since you only have a finite number of possible states and you always move from one state to another the proof of this becomes trivial. The worst case time complexity is the same as the number of possible states.

On Wednesday, 18 June 2014 at 20:58:46 UTC, Ola Fosheim Grøstad
wrote:
> On Wednesday, 18 June 2014 at 15:25:11 UTC, Luís Marques wrote:
>> Maybe I missed something in this discussion, but unless you are
>> not including jumps/loops in those N instructions, just because
>> the number of instructions and memory is bounded does not mean
>> you can prove (for arbitrary programs) that the program
>> terminates.
>
> Yes, you can. You just run it until it enters a previous state. At that point you have an infinite loop and it won't terminate.
>
> Since you only have a finite number of possible states and you always move from one state to another the proof of this becomes trivial. The worst case time complexity is the same as the number of possible states.

Granted infinite resources. Good, now that we ruled that thing
out, can we talk about the subject, or do we need to continue
talking about imaginary things ?