On 11/20/2017 5:03 PM, Mark wrote:
> On Monday, 20 November 2017 at 22:56:44 UTC, Walter Bright wrote:
>> On 11/20/2017 3:27 AM, Timon Gehr wrote:
>>> On 20.11.2017 11:07, Atila Neves wrote:
>>>> The problem with null as seen in C++/Java/D is that it's a magical value that different types may have. It breaks the type system.
>>>
>>> In Java, quite literally so. The Java type system is /unsound/ because of null. (I.e. Java is only memory safe because it runs on the JVM.)
>>
>> I'm curious. Can you expand on this, please?
>>
>> (In D, casting null to any other pointer type is marked as @unsafe.)
> 
> This blog post seems to summarize the paper he linked to:
> https://dev.to/rosstate/java-is-unsound-the-industry-perspective

Thank you.

On Tuesday, 21 November 2017 at 01:03:36 UTC, Mark wrote:
> On Monday, 20 November 2017 at 22:56:44 UTC, Walter Bright wrote:
>> On 11/20/2017 3:27 AM, Timon Gehr wrote:
>>> On 20.11.2017 11:07, Atila Neves wrote:
>>>> The problem with null as seen in C++/Java/D is that it's a magical value that different types may have. It breaks the type system.
>>> 
>>> In Java, quite literally so. The Java type system is /unsound/ because of null. (I.e. Java is only memory safe because it runs on the JVM.)
>>
>> I'm curious. Can you expand on this, please?
>>
>> (In D, casting null to any other pointer type is marked as @unsafe.)
>
> This blog post seems to summarize the paper he linked to:
> https://dev.to/rosstate/java-is-unsound-the-industry-perspective

And, like clockwork, the very first post is someone complaining that he insulted Javascript with an offhand example with a thread going 10 posts deep.

I'm not clear on whether he means that Java's type system is unsound, or that the type checking algorithm is unsound. From what I can tell, he's asserting the former but describing the latter.

On Tuesday, 21 November 2017 at 06:03:33 UTC, Meta wrote:
> On Tuesday, 21 November 2017 at 01:03:36 UTC, Mark wrote:
>> On Monday, 20 November 2017 at 22:56:44 UTC, Walter Bright wrote:
>>> On 11/20/2017 3:27 AM, Timon Gehr wrote:
>>
>> This blog post seems to summarize the paper he linked to:
>> https://dev.to/rosstate/java-is-unsound-the-industry-perspective
>
> I'm not clear on whether he means that Java's type system is unsound, or that the type checking algorithm is unsound. From what I can tell, he's asserting the former but describing the latter.

The spec describes unsound language, the hole in type-system are plugged at VM level by run-time checks.

Also this jawel:

Cat[] cats = new Cat[3];
...
Animals[] animals = cats; // the same array

animals[0] = new Dog();

cats[0].smth(); // ClassCast exception or some such

On Tuesday, 21 November 2017 at 06:03:33 UTC, Meta wrote:
> I'm not clear on whether he means that Java's type system is unsound, or that the type checking algorithm is unsound. From what I can tell, he's asserting the former but describing the latter.

He claims that type systems with existential rules, hierarchical relations between types and null can potentially be unsound. His complaint is that if Java had been correctly implemented to the letter of the spec then this issue could have led to heap corruption if exploited by a malicious programmer.

Runtime checks are part of the type system though, so it isn't unsound as implemented as generated JVM does runtime type checks upon assignment.

AFAIK the complaint assumes that information from generic constraints isn't kept on a separate level.

It is a worst case analysis of the spec...

On Tuesday, 21 November 2017 at 09:12:25 UTC, Ola Fosheim Grostad wrote:
> On Tuesday, 21 November 2017 at 06:03:33 UTC, Meta wrote:
>> I'm not clear on whether he means that Java's type system is unsound, or that the type checking algorithm is unsound. From what I can tell, he's asserting the former but describing the latter.
>
> He claims that type systems with existential rules, hierarchical relations between types and null can potentially be unsound. His complaint is that if Java had been correctly implemented to the letter of the spec then this issue could have led to heap corruption if exploited by a malicious programmer.
>
> Runtime checks are part of the type system though, so it isn't unsound as implemented as generated JVM does runtime type checks upon assignment.
>
> AFAIK the complaint assumes that information from generic constraints isn't kept on a separate level.
>
> It is a worst case analysis of the spec...

I don't quite understand the logic here, because it seems to be backwards reasoning. Constrain<U,? super T> is a valid type because null inhabits it? That doesn't make sense to me. He also cites the "implicit constraint" that X extends U where X is ? super T, but X does not meet that constraint (Constrain<U, X extends U>) so how can  the type checker deduce that X extends U?

On Tuesday, 21 November 2017 at 18:00:37 UTC, Meta wrote:
> I don't quite understand the logic here, because it seems to be backwards reasoning. Constrain<U,? super T> is a valid type because null inhabits it? That doesn't make sense to me. He also cites the "implicit constraint" that X extends U where X is ? super T, but X does not meet that constraint (Constrain<U, X extends U>) so how can  the type checker deduce that X extends U?

I haven't dug into the details of the paper as I think the authors didn't try to appear neutral, e.g. quoting null as the billon dollar mistake, and made their finding seem more spectacular than it is… What I get from skimming over it is this:

You get a call:

    upcast(constrain,x) -> String

   where:
       constrain is of type Constrain<String, X>
       x is of type X  (X is unspecified supertype of Integer)
       return type is String, which has X as subclass

   So you get String <: X <: Integer

The deduction that String is a superclass of Integer could come from:
    Constrain<String, X>

   where X = ? super Integer = unknown type that is supertype of Integer

On 19.11.2017 23:54, Walter Bright wrote:
> ... > There's also an issue of how to derive a class from a base class.
> ...

How so?

While we are talking applicability to D: The main issue is to ensure that fields of objects are initialized properly before being accessed. D already needs to do this, but fails, which means references to immutable data are not guaranteed to yield consistent results between dereferences.

> 
>>>>> What should the default initializer for a type do?
>>>> There should be none for non-nullable types.
>>> I suspect you'd wind up needing to create an "empty" object just to satisfy that requirement. Such as for arrays of objects, or objects with a cyclic graph.
>> Again, just use a nullable reference if you need null. The C# language change makes the type system strictly more expressive. There is nothing that cannot be done after the change that was possible before, it's just that the language allows to document and verify intent better.
> 
> This implies one must know all the use cases of a type before designing it.
> ...

No. The opposite is the case: you can just change the type once the requirements change. Then the type system shows you precisely where you need to update your code. In D, such a change is quite hard to make.

> 
>>> Yes, my own code has produced seg faults from erroneously assuming a value was not null. But it wouldn't have been better with non-nullable types, since the logic error would have been hidden
>>
>> It was your own design decision to hide the error.
> 
> No, it was a bug. Nobody makes design decisions to insert bugs :-) The issue is how easy the bug is to have, and how difficult it would be to discover it.
> ...

You added a special invalid instance that does not blow up on dereference. That was a conscious design decision. If your point is that there can be bugs unrelated to null, well that's unrelated to null.

> 
>>> and may have been much, much harder to recognize and track down.
>> No, it would have been better because you would have been used to the more explicit system from the start and you would have just written essentially the same code with a few more compiler checks in those cases where they apply, and perhaps you would have suffered a handful fewer null dereferences.
> 
> I'm just not convinced of that.
> ...

I'm confident that you would be able to use null safe languages properly if that is what had been available for most of your career.

> 
>> The point of types is to classify values into categories such that types in the same category support the same operations. It is not very clean to have a special null value in all those types that does not support any of the operations that references are supposed to support. Decoupling the two concepts into references an optionality gets rid of this issue, cleaning up both concepts.
> 
> I do understand that point. But I'm not at all convinced that non-nullable types in aggregate results in cleaner, simpler code, for reasons already mentioned.
> ...

I guess that depends on one's definition of clean and simple. Using nullable references for passing around references known to be non-null is not clean in my book.

>>> I wish there was a null for int types.
>> AFAIU, C# will now have 'int?'.
> 
> Implemented as a pointer to int? That is indeed one way to do it, but rather costly.
> ...

It lowers to Nullable<int>, which is a struct with a boolean flag.

> 
>> It can also be pretty annoying.
> 
> Yes, it can be annoying, so much better to have a number that looks like it might be right, but isn't, because 0.0 was used as a default initializer when it should have been 1.6. :-)
> ...

That's not what I was saying.

> 
>> It really depends on the use case. Also this is in direct contradiction with your earlier points. NaNs don't usually blow up.
> 
> "blow up" - as I've said many times, I find the visceral aversion to seg faults puzzling.

This is a misinterpretation. My language does not carry implicit emotional context during technical discussions. Given that you have a bug, blowing up is often the ideal outcome. It is even better to not have the bug in the first place. That's what explicit null (often) does for you.

(Also, I'd posit the reason why you don't understand why segfaults can be very painful to some is that you are in the compiler business.)

> Why is that worse than belatedly discovering a NaN in your output, which you now have to back search it to its source?
> ...

That is the opposite of the point I was making. You said: "bugs should terminate the program" and then "NaNs are underused". If my program calls 'std.math.log' with an argument of '-123.4', then that's probably a bug, so there seemed to be an inconsistency.

> My attitude towards programming bugs is to have them immediately halt the program as soon as possible, so:
> ...

My attitude is that ideally they are catched even sooner, during design time or compilation.

You are contrasting bugs that produce incorrect outputs and bugs that crash your program. It's the wrong comparison to make. It does not help to point the finger at an unrelated issue. Null safety turns bugs that crash the program into compilation errors.

(Note that there are type system features that allow you to automatically verify the program logic during compilation, but this is even further away from what I consider to be realistic to expect to see in D.)

> 1. I know an error has occurred, i.e. I don't get corrupt results that I assumed were correct, leading to more adverse consequences
> 2. The detection of the error is as close as possible to where things went wrong
> 
> Having floats default initialize to 0.0 is completely anti-ethical to (1) and (2),

Agreed.

> and NaN at least addresses (1).
> ...

It does not really. Comparison of NaNs yields a standard boolean value.

On 21.11.2017 07:46, Dmitry Olshansky wrote:
> 
> The spec describes unsound language, the hole in type-system are plugged at VM level by run-time checks.
> 
> Also this jawel:
> 
> Cat[] cats = new Cat[3];
> ...
> Animals[] animals = cats; // the same array
> 
> animals[0] = new Dog();
> 
> cats[0].smth(); // ClassCast exception or some such
> 

Actually, the "java.lang.ArrayStoreException" will be thrown already when you attempt to add the dog to the cat array. This is by design though (and explicitly supported by the JVM). The reason why the null-related Java type system hole does not lead to memory corruption is that the JVM does not support generics. (It's all translated to explicit type casts that are expected to always succeed, but the JVM still checks them.)

On Tuesday, 21 November 2017 at 20:02:06 UTC, Timon Gehr wrote:
>
> I'm confident that you would be able to use null safe languages properly if that is what had been available for most of your career.
>

You do realise, that all of the issues you mention can just be handled by coding correctly in the first place.

If your program calls 'std.math.log' with an argument of '-123.4', then that's probably NOT a bug. It's more likely to be incorrect code. Why not bounds-check the argument before passing it to the function?

If you access a field of an invalid instance of an object, that's probably NOT a bug. It's more likely to be incorrect code. Before you access a field of an object, check that the object is valid.

Its seems to be, that you prefer to rely on the type system, during compilation, for safety. This is very unwise.

btw. what was the last compiler you wrote?

On Wednesday, 22 November 2017 at 00:19:51 UTC, codephantom wrote:
> Its seems to be, that you prefer to rely on the type system, during compilation, for safety. This is very unwise.
>

To demonstrate my point, using code from a 'safe' language (C#):
(i.e. should this compile?)

// --------------------------------------------------

using System;

public class Program
{


    public static int Main()
    {
        Foo();
        return 0;
    }

    static void Foo()
    {
        const object x = null;

        //if (x != null)
        //{
            Console.WriteLine(x.GetHashCode());
        //}
    }

}

// --------------------------------------------------