Hacker News Reader

The timsort bug:

http://www.envisage-project.eu/proving-android-java-and-pyth...

Most software that's correctness critical is not written in Java.

But I could see KeY-verified voting machines as at least better than the status quo (as long as you take it as an assumption that for whatever reason we absolutely need voting machines).

View on HN

But alas:

> The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space.

Reply on news.ycombinator.com