Formal verification of software: We know that no responsible scientist guesses his formulae but derives them and in the same vein we derive our programs by for

Formal verification of software: We know that no responsible scientist guesses his formulae but derives them and in the same vein we derive our programs by formal calculation. This is a time-honoured tradition, formalization is just a matter of intellectual hygiene, and we should be quite confident that, indeed, this undertaking makes all the sense in the world, but we hesitate and are ambivalent about it because, all around us, our hygienic practices are opposed, derided and ridiculed.