June 07, 2016
On 6/7/16 5:10 PM, Jonathan M Davis via Digitalmars-d wrote:
> On Tuesday, June 07, 2016 20:52:15 Dave via Digitalmars-d wrote:
>> On Tuesday, 7 June 2016 at 20:48:13 UTC, Jonathan M Davis wrote:
>>> On Tuesday, June 07, 2016 18:33:01 Dave via Digitalmars-d wrote:
>>>> [...]
>>>
>>> IMHO, it's bad practice to mass apply attributes with labels or
>>> blocks. It's far too easy to accidentally mark a function with
>>> an attribute that you didn't mean to, and it makes it way
>>> harder to figure out which attributes actually apply to a
>>> function. And when you add templates into the mix, applying
>>> attributes en masse doesn't work anyway, because pretty much
>>> the only time that you want to mark a template function with an
>>> attribute is when the template arguments have nothing to do
>>> with whether the attribute is appropriate or not.
>>>
>>> [...]
>>
>> So we should not follow the advice of Walter?
>
> If he's arguing that you should slap an attribute on the top of your
> module to apply to everything, then no, I don't think that we should follow
> his advice. He's a very smart guy, but he's not always right. And in my
> experience, mass applying attributes is a mistake.
>

The original(?) complaint was that it's hard to grep for @system because it's the default.

I think the advice is to put the attribute at the top to see where your non-conforming code lies. Not as a permanent fixture.

I can attest that figuring out why something isn't inferred @safe isn't always easy, and the "slap a @safe: tag at the top" isn't always going to help. But it can be a technique to find such things.

-Steve
June 07, 2016
On Tuesday, June 07, 2016 17:28:27 Steven Schveighoffer via Digitalmars-d wrote:
> On 6/7/16 5:10 PM, Jonathan M Davis via Digitalmars-d wrote:
> > On Tuesday, June 07, 2016 20:52:15 Dave via Digitalmars-d wrote:
> >> On Tuesday, 7 June 2016 at 20:48:13 UTC, Jonathan M Davis wrote:
> >>> On Tuesday, June 07, 2016 18:33:01 Dave via Digitalmars-d wrote:
> >>>> [...]
> >>>
> >>> IMHO, it's bad practice to mass apply attributes with labels or blocks. It's far too easy to accidentally mark a function with an attribute that you didn't mean to, and it makes it way harder to figure out which attributes actually apply to a function. And when you add templates into the mix, applying attributes en masse doesn't work anyway, because pretty much the only time that you want to mark a template function with an attribute is when the template arguments have nothing to do with whether the attribute is appropriate or not.
> >>>
> >>> [...]
> >>
> >> So we should not follow the advice of Walter?
> >
> > If he's arguing that you should slap an attribute on the top of your
> > module to apply to everything, then no, I don't think that we should
> > follow
> > his advice. He's a very smart guy, but he's not always right. And in my
> > experience, mass applying attributes is a mistake.
>
> The original(?) complaint was that it's hard to grep for @system because
> it's the default.
>
> I think the advice is to put the attribute at the top to see where your non-conforming code lies. Not as a permanent fixture.
>
> I can attest that figuring out why something isn't inferred @safe isn't always easy, and the "slap a @safe: tag at the top" isn't always going to help. But it can be a technique to find such things.

Yeah. It makes sense as a temporary solution to track down problems. It makes a lot less sense as a way to write your code normally.

- Jonathan M Davis

June 08, 2016
On 07.06.2016 21:52, Walter Bright wrote:
> On 6/7/2016 11:32 AM, Timon Gehr wrote:
>> The @safe subset should be specified and
>> implemented by inclusion, such that it is obvious that it does the
>> right thing.
>> I don't know what's 'unspecific' about this.
>> Closing holes one-by-one is not the
>> right approach here. You don't know when you are done and might never be.
>
> I don't see how it is any different painting the fence from one
> direction or the other.

The fence is infinitely long, your painting speed is finite and people will be looking at the fence mostly at the left end.

> There are omissions possible either way.
> ...

In one way, an omission means you are potentially tracking down memory corruption inside a huge codebase by grepping for @trusted, until you notice that the issue is in @safe code.

In the other way, an omission means you are getting a spurious compile error that is easily worked around.

> Another issue is implementing such a spec. The "disapproved" list is how
> the compiler works,

It is how the compiler fails to work.

> and makes it reasonably straightforward to check the
> implementation against the list. It's quite a mess to try to tag
> everything the compiler does with approved/disapproved, so you wind up
> in exactly the same boat anyway.
> ...

The compiler should work by inclusion too.

> In any case, writing such a large specification covering every semantic
> action of the of the language is way, way beyond being a bugzilla issue.
> ...

Does not apply. The bugzilla issue can be fixed by disallowing all code in @safe. Also, why not just close the bugzilla issue _after_ there is a more adequate replacement?

> If you want to take charge of writing such a specification DIP,
> please do so.
>

If you think progress on this matters, why are you arguing against it?

June 08, 2016
On 07.06.2016 22:36, Walter Bright wrote:
> ...
>
> BTW, it is a nice idea to require mathematical proofs of code
> properties, but real world programming languages have turned out to be
> remarkably resistant to construction of such proofs. As I recall, Java
> had initially proven that Java was memory safe, until someone found a
> hole in it. And so on and so forth for every malware attack vector
> people find. We plug the problems as we find them.

Obviously they proved the virtual machine itself memory safe, not all of its implementations. If you have a mechanized proof of memory safety, then your language is memory safe.
June 07, 2016
On 6/7/2016 12:56 PM, Steven Schveighoffer wrote:
> Bug? I would have expected @nogc: to permeate.

It did originally, but that was removed. It's deliberate.
June 07, 2016
On 6/7/2016 11:32 AM, Timon Gehr wrote:
> mixin("@tru"~"sted void foo(){ ... }");

So grep for mixin, too. Not hard.

June 07, 2016
On 6/7/2016 3:23 PM, Timon Gehr wrote:
> Obviously they proved the virtual machine itself memory safe,

As I recall, the proof was broken, not the implementation. People do make mistakes and overlook cases with proofs. There's nothing magical about them.

June 08, 2016
On 08.06.2016 00:44, Walter Bright wrote:
> On 6/7/2016 11:32 AM, Timon Gehr wrote:
>> mixin("@tru"~"sted void foo(){ ... }");
>
> So grep for mixin, too. Not hard.
>

Huge amounts of false positives.
June 08, 2016
On 08.06.2016 00:47, Walter Bright wrote:
> On 6/7/2016 3:23 PM, Timon Gehr wrote:
>> Obviously they proved the virtual machine itself memory safe,
>
> As I recall, the proof was broken, not the implementation.

Which time?

> People do
> make mistakes and overlook cases with proofs. There's nothing magical
> about them.
>

Obviously, but there are reliable systems that check proofs automatically.
June 07, 2016
On Tuesday, June 07, 2016 15:47:10 Walter Bright via Digitalmars-d wrote:
> On 6/7/2016 3:23 PM, Timon Gehr wrote:
> > Obviously they proved the virtual machine itself memory safe,
>
> As I recall, the proof was broken, not the implementation. People do make mistakes and overlook cases with proofs. There's nothing magical about them.

Yeah. I recall an article by Joel Spoelsky where he talks about deciding that proofs of correctness weren't worth much, because they were even harder to get right than the software.

I do think that there are situations where proofs are valuable, but they do tend to be very difficult to get right, and their application is ultimately fairly limited.

- Jonathan M Davis