Proving Code Works with Z3
At the PyCon SG Education Summit today, Melvin’s lighting talk on “Writing Proofs in Python” began with a subtle bug in this mid-point calculation (often used in binary search or sort) in languages like Java, C/C++, Go, etc. low = ... high = ... mid = (low + high) / 2 Since the integers are fixed-width, this triggers an overflow when low + high exceeds the maximum integer value. Even popular libraries like Pandas had this bug until 2019. In fact, even Python’s native list.sort() had this sort of bug until 2015! Read the details. ...