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. ...

How IMF mis-forecasts GDP growth

The IMF forecasts GDP growth every year. Their forecasts for the current year are slightly low. Their forecasts for the next year are slightly high. After that, it remains high. Some forecasts, like China, Singapore, UAE, Equatorial Guinea are consistently low. Other forecasts, like Japan, Congo, Mexico, Pakistan are consistently high. The interesting meta-pattern is how this sort of past-forecast analysis can be done for any topic. This emerged from an Ethan Mollick post and then I asked: ...