You're technically correct, but in practice, proving that software does confirm to a formal specification is, empirically, a good way of drastically reducing defects.