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