волшебно

Некие люди занимались верификацией всякого кода на Джаве и столкнулись с трудностями при доказательстве корректности TimSort'a - алгоритма сортировки, издавна используемого в Питоне и Джаве. Оказалось, что он некорректен, на некоторых данных не работает вообще.

Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)

Кому вообще нужны эти теорем-пруверы? Питон, тесты, махание руками!