&gt; If we had just one artifact: a specification that executes, then there would be no concept of proof any more.<p>It is possible for an executable functional specification to have unbearably bad performance for production use. In that case, the programmer has to reimplement the program in a more efficient (but perhaps less obvious) way <i>and</i> supply a proof that the reimplementation is functionally equivalent to the original executable specification.<p>Proofs aren&#x27;t going away anytime soon.<p>&gt; There is only the question whether the specification that was expressed is the one that was intended <i>in the mind</i>.<p>If other people can&#x27;t bother communicating what they really want, that is absolutely Not My Problem (tm).<p>&gt; Plus, there is the external question of whether a specification has unintended consequences.<p>If other people can&#x27;t analyze the logical consequences of what they wish for, that is absolutely Not My Problem (tm). The most I can do is point at contradictions in the requirements.