I just read that the sort function in Java (and Python) does not work correctly for all possible inputs.

A function that is literally used billions of times has a bug nobody found until now? Yes. They found it by trying to formally prove its correctness. This works by annotating the source code with things as preconditions, postconditions and invariants. The system then statically verifies that they hold all the time.

The system said that they do not hold all the time and therefore, the function does not always what it should do. They even were able to say how to fix the problem, submitted a bug report and it’s already fixed in the trunk of OpenJDK.

Very interesting story. We see that

  • Creating correct programs is incredibly difficult.
  • Unit tests and also property based testing cannot find all classes of bugs.
  • Maybe Design by contract is not so bad an idea and should be more widely adopted? Also with the advent of REST and micro services there’s an increased need to define contracts. Not on a function or class level but between services. So more contracts for a better world?