This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions.
Really shines as an example of how important proof is in computer science.
Really shines as an example of how important proof is in computer science.