> C# apparently has a "checked" keyword [0] to enable overflow checking, which presumably would have prevented this as well. Java uses unsafe addition by defaul

> C# apparently has a "checked" keyword [0] to enable overflow checking, which presumably would have prevented this as well. Java uses unsafe addition by default but, since version 8, has the "addExact" static method [1] which makes it inconvenient but at least possible to write safe code. This is the point I'm making: verifying a program is separate from writing it. Constantly going back and saying "but-if we just X" is a distraction. Secure software is verified software, not bugfixed. And that's the point a lot of people don't like to acknowledge about software. It's not enough to remediate defects: you must prevent them in the first place. And that requires program verification, which is a dramatically different problem than the one OC thinks they're solving.