On 06/17/2014 11:50 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> ...
> Btw, Rice's theorem is based on the halting problem for TMs… so it
> suffers from the same issues as everything else in theoretical CS when
> it comes to practical situations.

There is no such 'issue', or any meaningful way to define a 'practical' situation, especially such that the definition would apply to the current context. Theoretical computer scientists are saying what they are saying and they know what they are saying.

> Whether generated IR contains unsafe
> instructions is trivially decidable. Since you can define an IR in a way
> that discriminate between unsafe/safe instructions you can also decide
> that the safe subset is verifiable memory safe.

As you know this will not single out _exactly_ the subset of programs which is memory safe which is the claim I was arguing against, and invoking Rice's theorem to this end is perfectly fine and does not suffer from any 'issues'. The kind of thing you discuss in this paragraph, which you appear to consider 'practical' is also studied in theoretical CS, so what's your point?

On Tuesday, 17 June 2014 at 22:44:00 UTC, Timon Gehr wrote:
> As you know this will not single out _exactly_ the subset of programs which is memory safe which is the claim I was arguing against,

It will single out exactly the programs that are most certainly memory safe, and also single out those programs that have generated unsafe features (instructions). Whether those unsafe features sit in a basic block that will never called is a different matter since @safe does not address that.

So yes, @safe is not equivalent to memory safety, it is equivalent to the absence of FEATURES that can lead to situations that aren't memory safe. But that is splitting hairs.

Absence of features such as unsafe instructions is a trivial property of the compiled program. A non trivial property is whether the program terminates, returns 0, rejects the input "hello", etc.

> and invoking Rice's theorem to this end is perfectly fine and does not suffer from any 'issues'.

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.

But this issue is simpler than that. Think about it this way: There are problems that have a solution, but it is provable impossible to solve analytically. You still can solve them numerically down to a specified precision.

I posit you can do the same with memory safety, as in: you can reject all unsafe programs and reduce the set of false positives to a marginal set of typical programs (which are written with memory safety in mind).

On Wednesday, 18 June 2014 at 06:35:01 UTC, Ola Fosheim Grøstad wrote:
> On Tuesday, 17 June 2014 at 22:44:00 UTC, Timon Gehr wrote:
>> As you know this will not single out _exactly_ the subset of programs which is memory safe which is the claim I was arguing against,
>
> It will single out exactly the programs that are most certainly memory safe, and also single out those programs that have generated unsafe features (instructions). Whether those unsafe features sit in a basic block that will never called is a different matter since @safe does not address that.
>
> So yes, @safe is not equivalent to memory safety, it is equivalent to the absence of FEATURES that can lead to situations that aren't memory safe. But that is splitting hairs.
>

That isn't splitting hair. You are loosing track of the big picture here. To come back to the original problem :

memset(&foo, 0, typeof(foo).sizeof);

Walter mention that this is not corrupting memory and therefore @safe. In the situation of tail pad optimization, it is obviously not valid anymore and will cause memory corruption. The discussion then derailed to what is @safe, as the code is certainly @safe, but it is difficult to prove it is automatically) 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 rather than listing what is allowed and adding to the list when some construct are proven to be @safe).

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!

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.

On Wednesday, 18 June 2014 at 06:50:14 UTC, deadalnix wrote:
> That isn't splitting hair. You are loosing track of the big picture here. To come back to the original problem :
>
> memset(&foo, 0, typeof(foo).sizeof);
>
> Walter mention that this is not corrupting memory and therefore @safe.

memset is by definition an unsafe feature, but a hypothetical cleartype(foo,…) is a safe feature. Imagine having a hypothetical IR that makes the unsafe/safe distinction, then you can have both memset and cleartype in that IR and transform them into memset at the lower level backend without causing problems for memory safety verification.

> In the situation of tail pad optimization, it is obviously not valid anymore and will cause memory corruption.

But if you have cleartype() when you do tail pad optimization and turn it into memset a codegen then you are ok?

> The discussion then derailed to what is @safe, as the code is certainly @safe, but it is difficult to prove it is automatically) 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 rather than listing what is allowed and adding to the list when some construct are proven to be @safe).

I don't disagree, I think the simplest thing to do is to have a hypothetical implied IR between the AST and the backend and accept safe features on that level.

I think people who care about @safe also will accept that some safe programs are rejected if it is easy to modify the code into something the compiler accepts. The compiler could even provide suggestions: ("consider using cleartype() over memset()" etc).

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!

On Wednesday, 18 June 2014 at 08:13:59 UTC, Walter Bright wrote:
> 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.

Lol, I'd love to see your response to them.

> 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!

I largely agree with this assessment, but would also like to point out that while almost all programmers use compilers, very few know how to improve one.  You can help by fleshing out the dmd source guide so that it's better, then pointing people at it when they demand stuff from you: ;)

http://wiki.dlang.org/DMD_Source_Guide

I know, more work for you and the few dmd contributors, but you guys can help others get involved with better documentation for dmd.

On 18/06/2014 8:52 p.m., Joakim wrote:
> On Wednesday, 18 June 2014 at 08:13:59 UTC, Walter Bright wrote:
>> 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.
>
> Lol, I'd love to see your response to them.
>
>> 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!
>
> I largely agree with this assessment, but would also like to point out
> that while almost all programmers use compilers, very few know how to
> improve one.  You can help by fleshing out the dmd source guide so that
> it's better, then pointing people at it when they demand stuff from you: ;)
>
> http://wiki.dlang.org/DMD_Source_Guide
>
> I know, more work for you and the few dmd contributors, but you guys can
> help others get involved with better documentation for dmd.

From my experience, one of the reasons I haven't had much to do with the development of dmd is simply to compile dmd, druntime is not as straight forward as it could be.
All I can say is with ddmd make it compilable with dub same goes with druntime. With a nice tutorial on how to set it all up on Windows/Linux ext.
Preferably with a nice automated means of, this is how we make a release build for platform x.

It'll go along way. It really would. And anyway it'll really show off the power of dub ;)

But in saying all this, I may want to learn to write my own compiler ext. I just don't have the knowledge and even getting into x86 instruction encoding is head hurting alone as it stands.

On Wednesday, 18 June 2014 at 09:16:32 UTC, Rikki Cattermole wrote:
> From my experience, one of the reasons I haven't had much to do with the development of dmd is simply to compile dmd, druntime is not as straight forward as it could be.
> All I can say is with ddmd make it compilable with dub same goes with druntime. With a nice tutorial on how to set it all up on Windows/Linux ext.
> Preferably with a nice automated means of, this is how we make a release build for platform x.

I used this guide from the wiki some time back to start building dmd/druntime/phobos and run their tests, pretty easy:

http://wiki.dlang.org/Building_DMD

Non-Windows builds are very easy.  Windows builds require a bit too much manual configuration, I'll agree with that.

> It'll go along way. It really would. And anyway it'll really show off the power of dub ;)

Daniel should stick his D frontend up there as a library, even if it isn't architected to be used as a library right now.  People will find ways to use it and his translated code will get some testing.