> If we had just one artifact: a specification that executes, then there would be no concept of proof any more. It is possible for an executable functional spe

> If we had just one artifact: a specification that executes, then there would be no concept of proof any more. 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 and supply a proof that the reimplementation is functionally equivalent to the original executable specification. Proofs aren't going away anytime soon. > There is only the question whether the specification that was expressed is the one that was intended in the mind. If other people can't bother communicating what they really want, that is absolutely Not My Problem (tm). > Plus, there is the external question of whether a specification has unintended consequences. If other people can'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.