Introduction

Abstract

There is a widespread misunderstanding among both software practitioners and experts in the area of formal methods that the purpose of such methods is to prove, conclusively, whether some piece of software is “correct”. This confusion is rather unfortunate, since it often leads to disillusionment and rejection of formality as impractical (e.g., it does not scale) and, therefore, irrelevant to software development. In fact, as the quote from Alfred North Whitehead indicates, the notion of conclusive and objective proof derived by formal methods has been all but abandoned even in mathematics itself, where it is now understood that “proofs” really represent social consensus among mathematicians rather than statements of objective reality. This should be even more apparent in the case of mathematical models of real-world systems, which are almost always approximations of some kind.