This is a much clearer argument to me. Theorem provers can be used to ensure certain constraints are met for all possible inputs. It doesn't matter to a theorem

This is a much clearer argument to me. Theorem provers can be used to ensure certain constraints are met for all possible inputs. It doesn't matter to a theorem prover if 1/0=0, 1/0=infinity, or 1+1=3 so long as you can show the system stays within its constraints. It's not a question of math, it's about what you can prove the machine will do. I believe most of us doing systems programming and building control systems use IEEE 754, so it's surprising to see a conflicting suggestion. I'd say the biggest thing is that programmers need to be aware of how 1/0 is handled, as 0, infinity, or an exception can all cause undesired results.