No, it's just impossible in some cases, and you don't know which cases. If the validator fails to work, the target software is too vague and has to be re-writte

No, it's just impossible in some cases, and you don't know which cases. If the validator fails to work, the target software is too vague and has to be re-written. But you can write software that can be proven to be correct. You can also write software that can be proven to stay within certain limits (i.e. the computer will fiddle with the acceleration a bit, but not more than a reasonable pre-defined limit, and not when the brake is on).