> if your axioms are violated by your system then your system can wind up in an undefined state. Yes, and if your hardware is broken or a cosmic ray hits your

> if your axioms are violated by your system then your system can wind up in an undefined state. Yes, and if your hardware is broken or a cosmic ray hits your system in just a bad way, then all the static type checking in the world won't help against that. But that's a different problem to solve, isn't it? I'd postulate that for most applications, you'd usually be happy to have a software stack that's less likely to contain programming bugs in the first place. It's also true that you don't want faulty Airbag software in your car to affect your steering, but don't you want non-faulty Airbag software as well?