It's also difficult because software despite being a realm of abstract constructs still exists in the physical world. Hardware corruption can introduce bugs des

It's also difficult because software despite being a realm of abstract constructs still exists in the physical world. Hardware corruption can introduce bugs despite the software being formally correct. It's fascinating learning about hardware manufacturing for satellites and needing to build in hardware redundancy and error checking for bits getting flipped by solar radiation. And of course there was the famous rowhammer attack. So you need not just software expertise but also hardware expertise if you're going to get serious about writing error-proof code, which Dan Bernstein happens to have.