Java and Scala are Unsound

[Ross Tate]

I just realized none of y'all are on Facebook (or at least use it much) and so never saw this. It'll be appearing at OOPSLA, though I'm still finishing the final version.

https://www.dropbox.com/s/7ulph57piidj2qj/paper.pdf?dl=0

I don't think this bug applies to Ceylon for multiple reasons, but let me know if you come up with a concern.

Cheers!

Ross

[Gavin King]

Can I tweet this?

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-dev+...@googlegroups.com.
> To post to this group, send email to ceylo...@googlegroups.com.
> Visit this group at https://groups.google.com/group/ceylon-dev.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ceylon-dev/CABnofR6-y8E%3DELTKwweLi409mhAeRrgkysdv8hUD7GtCSQO5VA%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.



--
Gavin King
ga...@ceylon-lang.org
http://profiles.google.com/gavin.king
http://ceylon-lang.org
http://hibernate.org
http://seamframework.org

[Ross Tate]

Wait a bit - I'm not supposed to distribute this broadly yet. I wanted to give y'all the draft first in case you had any suggestions. I'll have the finished one soon, which you can certainly tweet!

On Wed, Aug 17, 2016 at 4:54 PM, Gavin King <gavin...@gmail.com> wrote:

Can I tweet this?

On Wed, Aug 17, 2016 at 9:03 PM, Ross Tate <ro...@ceylon-lang.org> wrote:
> I just realized none of y'all are on Facebook (or at least use it much) and
> so never saw this. It'll be appearing at OOPSLA, though I'm still finishing
> the final version.
>
> https://www.dropbox.com/s/7ulph57piidj2qj/paper.pdf?dl=0
>
> I don't think this bug applies to Ceylon for multiple reasons, but let me
> know if you come up with a concern.
>
> Cheers!
> Ross
>

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to ceylon-dev+unsubscribe@googlegroups.com.

> To post to this group, send email to ceylo...@googlegroups.com.
> Visit this group at https://groups.google.com/group/ceylon-dev.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ceylon-dev/CABnofR6-y8E%3DELTKwweLi409mhAeRrgkysdv8hUD7GtCSQO5VA%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.

--
Gavin King
ga...@ceylon-lang.org
http://profiles.google.com/gavin.king
http://ceylon-lang.org
http://hibernate.org
http://seamframework.org

--
You received this message because you are subscribed to the Google Groups "ceylon-dev" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+unsubscribe@googlegroups.com.

To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/CAP7PoCeG52cQsTk1SCacNSHb1KxdtKWp%3DhSf8T1nB7b5Rv%3DCyw%40mail.gmail.com.

[Lucas Werkmeister]

Very interesting, this. Thanks for the link!

I especially like how 6.3 provides additional justification for https://github.com/ceylon/ceylon/issues/3641. Were you already working on this paper when you made that suggestion? :)

Three minor comments. This, near the end of section 3:

> Without knowing that T is a subtype of U, it is impossible to create such an instance. So type-checking the method invocation could actually be sound since it might not be unreachable.

Don’t you mean “might not be reachable” or “might be unreachable”? Then it would make sense to me – if soundness is about everything “working out” at runtime (I’m sorry, I don’t know the formal definition), and the code never runs, it needn’t influence soundness.

And at the beginning of section 7:

> Of course, any fix to unsoundness has to be backwards compatible in theory, so one must determine and take into account how these languages are used in practice.

Would an actual fix not have to be backwards *in*compatible? Any change that is to truly fix the problem must disallow your programs, right? And if I understand the term correctly, that would in theory mean backwards incompatibility (though, perhaps, an acceptable instance, if it did not break any programs “in practice”).

And I think the tilde in ?~super near the end of In Java should be a space, right? I assume that’s meant to be a LaTeX no-break space :)

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+...@googlegroups.com.

To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/CABnofR6Fc6Xbq4NYCEOnaL-u4x1g%3DtSzutmn3xoYg3xO9KcZog%40mail.gmail.com.

[Gavin King]

OK.

Sent from my iPhone

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+...@googlegroups.com.

To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/CABnofR6Fc6Xbq4NYCEOnaL-u4x1g%3DtSzutmn3xoYg3xO9KcZog%40mail.gmail.com.

[Ross Tate]

Whoa, nice catches! All fixed. Thanks, Lucas!

As for constraints, it's actually the other way around. I figured out they were unnecessary a while ago, back when I was simultaneously a developer and a PhD student, but I never had a way to publish them. So y'all found out long before academia did. Actually, y'all find out a lot of things before academia does ;-) But now I finally figured out a way to sneak it into a paper :-D

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+unsubscribe@googlegroups.com.

To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/CABnofR6Fc6Xbq4NYCEOnaL-u4x1g%3DtSzutmn3xoYg3xO9KcZog%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "ceylon-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+unsubscribe@googlegroups.com.
To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/5862da2c-82f8-64bd-a7be-fe501777c546%40googlemail.com.

[Paul Ebermann]

Hi,

maybe a bit late, but I just now got to reading this:

Ross Tate wrote:
> I just realized none of y'all are on Facebook (or at least use it much)
> and so never saw this. It'll be appearing at OOPSLA, though I'm still
> finishing the final version.
>
> https://www.dropbox.com/s/7ulph57piidj2qj/paper.pdf?dl=0

I guess in Figure 4 you want to call UnsoundSpec.coerce(), not
Unsound.coerce() in the main method.


Paul

[Ross Tate]

Ah! Thanks!

--
You received this message because you are subscribed to the Google Groups "ceylon-dev" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+...@googlegroups.com.

To post to this group, send email to ceylo...@googlegroups.com.
Visit this group at https://groups.google.com/group/ceylon-dev.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-dev/cabaa836-3bcd-d1f7-b9d3-de3fc6e421b2%40gmx.de.

[Ross Tate]

Alright, we finally got it through the publishers. And we made a cool website where you can run the examples yourself or make your own! Let me know if you come up with any cool variants :)

http://io.livecode.ch/learn/namin/unsound

Tweet: https://twitter.com/ninjividual/status/783771669445898240

And thanks again for the help!

Ross

On Thu, Sep 1, 2016 at 3:00 PM, Ross Tate <ro...@cs.cornell.edu> wrote:

Ah! Thanks!

On Wednesday, August 31, 2016, Paul Ebermann <Paul-E...@gmx.de> wrote:

Hi,

maybe a bit late, but I just now got to reading this:

Ross Tate wrote:
> I just realized none of y'all are on Facebook (or at least use it much)
> and so never saw this. It'll be appearing at OOPSLA, though I'm still
> finishing the final version.
>
> https://www.dropbox.com/s/7ulph57piidj2qj/paper.pdf?dl=0

I guess in Figure 4 you want to call UnsoundSpec.coerce(), not
Unsound.coerce() in the main method.


Paul

--
You received this message because you are subscribed to the Google Groups "ceylon-dev" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-dev+unsubscribe@googlegroups.com.