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 assume the matter has been long fixed by now, do you happen to know?
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
