On Thursday, 19 June 2014 at 18:10:57 UTC, Walter Bright wrote:
> On 6/19/2014 4:12 AM, Artur Skawina via Digitalmars-d wrote:
>> On 06/18/14 18:42, Dicebot via Digitalmars-d wrote:
>>> 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?
>>
>> Well, do you think I would have said what I did if this issue didn't
>> affect /me/? [1]
>
> The front end is now Boost licensed.

Admittedly his concerns are unclear, but his problem is with the backend, not the frontend, which he already said he likes better now that it's boost-licensed.  He claims that the proprietary backend scares potential contributors away and that it should be "split up" from the frontend, by which he might mean putting it in a separate git repo?

I don't know enough about these copyright tainting concerns to say if it's a good idea, just pointing out that he was talking about the backend, not the frontend.

On Thursday, 19 June 2014 at 19:12:53 UTC, Ola Fosheim Grøstad
wrote:
> You are being silly. You either discuss computability or you discuss complexity. Please don't mix the two topics.
>

Do you have something to contribute to THIS discussion, or ill
you continue to bring irrelevant topic in ?

On 06/19/2014 06:06 AM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> ...
> In the real world you work with typical programs that run on finite
> resources guided by heuristics. There is no proof that you cannot have
> @safe.

I assume you mean @safe <===> memory safety.

> So leave that line of arguing. It is fundamentally flawed.

No, your line of reasoning is flawed. The amount of resources is not a constant. You must prove that memory safety holds for _each possible_ amount of resources at which point you haven't won anything by talking about resource usage, or else you need to set an explicit resource bound _at the language level_ and enforce it.

On Thursday, 19 June 2014 at 19:37:32 UTC, H. S. Teoh via Digitalmars-d wrote:
> But the non-solvability of the halting problem means that there is no
> algorithm that can compress every possible program.

Even if true, programmers don't write every possible program when they try to write @safe code.

On 06/19/2014 09:06 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Thursday, 19 June 2014 at 18:25:00 UTC, Tobias Pankrath wrote:
>> It's not. Since the resources to verify a property are limited, too.
>>
>> If I need to enumerate all possible program states, there will always
>> exists a program that can run on my box but will not be verifiable on
>> it (since I lack the resources).
>
> Nobody have said you should enumerate all possible states.
>
> There's a significant difference between a proof and an algorithm.

I don't think it is that significant. They are basically the same except that the proof is typically more strongly typed and you cannot actually execute a proof by excluded middle in the general case.

On Thursday, 19 June 2014 at 20:26:27 UTC, Timon Gehr wrote:
> I assume you mean @safe <===> memory safety.

I mean that the best route in general is: @safe => memory safe features on the local level (trivial) => "strength reduction" into memory safe use of memory unsafe features (trivial).

> No, your line of reasoning is flawed. The amount of resources is not a constant. You must prove that memory safety holds for

I have not set out to prove anything, I dislike how people abuse CS in order to "win" an argument. If you guys want to leverage CS theory do it properly or leave it out. Just because you have read Garey and Johnson does not mean that you should leverage it without proper treatment.

On Thu, Jun 19, 2014 at 08:31:53PM +0000, via Digitalmars-d wrote:
> On Thursday, 19 June 2014 at 19:37:32 UTC, H. S. Teoh via Digitalmars-d wrote:
> >But the non-solvability of the halting problem means that there is no algorithm that can compress every possible program.
> 
> Even if true, programmers don't write every possible program when they try to write @safe code.

So how do you, as a compiler writer, predict exactly which programs your users will write? -- because without knowing that, you cannot know which analysis algorithms to implement that will solve the N-step halting problem for all the programs that users will write (even though that's only a very small finite set out of the space of all possible programs!). So the only remaining approach is to consider all possible programs. Which means you have to implement exhaustive state space search. Which is impractical for the reasons I stated.


T

-- 
This is a tpyo.

On Thursday, 19 June 2014 at 20:47:16 UTC, H. S. Teoh via Digitalmars-d wrote:
> programs!). So the only remaining approach is to consider all possible
> programs. Which means you have to implement exhaustive state space
> search. Which is impractical for the reasons I stated.

No. Is a program compiled to asm.js memory safe? It has to be, because Javascript is a memory safe environment.  You might still mess up badly, but you can obviously transform just about any program that is presumed to be memory unsafe into one that is memory safe (if you consider a function to be a mapping of input to output).

Are you telling me that you cannot write an equivalent mapping from input to output using memory safe primitives while staying within P? You can safely insist on only having access to valid memory safe primitives within @safe and still be able to solve the exact same problems, in pretty much the same way (on an abstract algorithmic level).

It's not like @safe guards against exceptions IIRC. You can inject bound checks everywhere and it is provable memory safe. @safe should guarantee that your program terminates in an orderly fashion without corrupting memory. @safe does not guarantee correctness. That would be a folly.

A hypothetical and pointless "not @safe" does not guarantee memory corruption either. If you compile to asm.js you obviously always stay memory safe.

Or do you define "out of array bounds" exceptions as memory corruption?

Now, if we were talking untransformable machine language, you might have a point, not sure. But we aren't talking machine language, we are talking D.

On 06/19/2014 10:39 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Thursday, 19 June 2014 at 20:26:27 UTC, Timon Gehr wrote:
>> ...
>> No, your line of reasoning is flawed. The amount of resources is not a
>> constant. You must prove that memory safety holds for
>
> I have not set out to prove anything,

This is a discussion about proving memory safety.
(Though this is not at all apparent from the original topic. This sort of went out of hand. :o))

> I dislike how people abuse CS in order to "win" an argument.

Sorry for having "won" the argument if that is what you are implying. That was not my intention and this is not actually a contest. My intention was to defend the use of properties of Turing machines in the context of a Turing complete programming language. I wanted to convey the message that it has no "issues" and it is not "fundamentally flawed". I also don't think I am guilty of "abuse".

> If you guys want to leverage CS theory do it
> properly or leave it out. Just because you have read Garey and Johnson

I haven't, if that helps.

> does not mean that you should leverage it without proper treatment.

I failed to decipher this part of the sentence. Is it just some more boring name calling or is there an insight behind it?


NB: I have started to write down a complete-ish list of @safe language features and I will post them to the issue opened by H.S. Teoh soon.

On 06/19/2014 11:28 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> But we aren't talking machine language, we are talking D.

This part is spot on.