3 ms·
Proving that a code always works means that there doesn't exist any case in which it breaks. You can't really prove something doesn't exist, unless the input do
by XCSme 4y ago
Proving that a code always works means that there doesn't exist any case in which it breaks. You can't really prove something doesn't exist, unless the input domain is of fixed size and you can test all of it. In self-hosted technology, it is even trickier to prove something won't break, as there is so much potential variation in the hardware/software that your program runs on. There might even be stupid edge-cases, like the program failing only when the device it runs on is upside-down, or placed at high altitude, etc.
- rowanG077 4y agoYou can prove things even if then input domain has infinite size. For example n < n + 1 is always true. It's trivial to prove this. Yet the n can have infinite different values.
- naikrovek 4y agoIs this what "formal verification" is? That seems very hard for software that accepts arbitrary input. I understand formal verification, a bit, in terms of FPGA design, but not software.