Why not?

Too many possible inputs, even for small programs.

Testing increases our confidence that the program is ok.

Formal methods uses proofs to establish correctness

• ... but is the proof itself correct?