On 08.06.2016 01:07, Andrei Alexandrescu wrote:
On 6/8/16 12:53 AM, Timon Gehr wrote:
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?
That is an old result that has essentially expired and should not be
generalized. See
http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html.
I think this can't be what Walter is referring to: "the type inference
system for generic method calls was not subjected to formal proof. In
fact, it is unsound,"
I.e. no proof, unsound.
I assume the matter has been long fixed by now, do you happen to know?
...
I don't know.
BTW, Java's type system is unsound [1].
class Unsound {
static class Bound<A, B extends A> {}
static class Bind<A> {
<B extends A> A bad(Bound<A,B> bound, B b) {return b;}
}
public static <T,U> U coerce(T t) {
Bound<U,? super T> bound = null;
Bind<U> bind = new Bind<U>();
return bind.bad(bound, t);
}
public static void main(String[] args){
String s=coerce(0);
}
}
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.
It is my opinion that writing off formal proofs of safety is a mistake.
Clearly we don't have the capability on the core team to work on such.
However, I am very interested if you'd want to lead such an effort.
Andrei
I'll probably do it at some point. (However, first I need to figure out
what the formal language specification should actually be, this is one
reason why I'm implementing a D compiler.)
[1] https://www.facebook.com/ross.tate/posts/10102249566392775.
