>This is preventable if you specify fully what you actually want to do. In this case it was fully specified that sudo should run rm with all privileges, which

>This is preventable if you specify fully what you actually want to do. In this case it was fully specified that sudo should run rm with all privileges, which in turn will recursively deleted the root filesystem. The entire execution is fully specified and will execute without fault. There is no mistake in `sudo rm -rf /`. Logical faults may not be preventable with provers, such as when underlying assumptions are wrong. For example, a prover could have verified the parity library as fully okay because it assumes that the initialization function will not be called without delegation. This underlying assumption X -!> Y (X cannot lead to Y) is wrong and X -> Y is the case but the prover only verified that Y -!> X. Provers essentially duplicate your code, forcing you to express the solution and/or problem twice such that if you basically typo on the way, one of the pieces will complain about the other. But it cannot and is incapable of preventing higher level mistakes.