The whole mess of Boing is going further than originally thought. This makes me deeply uncomfortable, as I always regarded aviation as the one sector where people have time and budget to thoroughly test their software. Aviation was even the example #1 when it came to formal proving of algorithms, back in university.