如何看待Python/Java的排序算法被发现有潜在的bug

仔细读一下文章就知道啊…
简单说这个团队使用了一种半自动化的形式化分析方法对排序算法的有效性进行了验证，并且在验证过程中发现了bug，且提出了逻辑上合理的解决方法。
文末也进行了很好的总结：

1. Formal methods are often classified as irrelevant and/or impracticable by practitioners. This is not true: we found and fixed a bug in a piece of software that is used by billions of users every single day. Finding and fixing this bug without a formal analysis and the help of a verification tool is next to impossible, as our analysis showed. It has been around for years in a core library routine of Java and Python. Earlier occurrences of the underlying bug were supposedly fixed, but actually only made its occurrence less likely.
2. Even though the bug itself is unlikely to occur, it is easy to see how it could be used in an attack. It is likely that more undetected bugs are in other parts of core libraries of mainstream programming languages. Shouldn’t we try to find them before they can do harm or they can be exploited?
3. 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. Given the astronomical number of program runs that such a central routine is used in, this leads to a considerable waste of energy. As to the reasons, why our solution has not been adopted, we can only speculate: perhaps the JDK maintainers did not bother to read our report in detail, and therefore don’t trust and understand our fix. After all, Open Java is a community effort, largely driven by volunteers with limited time.
简单胡乱翻译：
1、形式化（分析）方法被证明是可行的，且有效的。这次的bug不使用形式化分析是很难通过只注重结果的测试方法发现的。事实上这个排序算法被使用了这么久也没有发现这个问题，证明了非形式化分析方法的不足。
2、此类bug虽然难以在日常使用中发生，但很容易利用类似bug制作攻击。所以我们应该寻找并消灭它们。
3、Java开发者社区并未采纳提议的修复方法，而是简单地采取了增大runLen数组的方法。作者对此很不高兴，并表达了一些不友好的臆测。
其实我就想
@RednaxelaFX
大神问一下为什么Java不愿意使用这个fix而倾向使用增加内存分配。

个人以为它们使用的KeY系统是一个非常好的尝试，个人粗浅的见地里大概是最好的形式化分析的应用。Java作为一门足够开放的语言对形式化方法的自动化提供了足够的基础，喜闻乐见。JML功不可没。