 From what has been said so far, it follows that correctness of implemented programs does not automatically establish the well-functioning of a computational system. Turing (1950) already distinguished between errors of functioning and errors of conclusion. The former are caused by a faulty implementation unable to execute the instructions of some high-level language program; errors of conclusion characterize correct abstract machines that nonetheless fail to carry out the tasks they were supposed to accomplish. This may happen in those cases in which a program instantiates correctly some specifications which do not properly express the users’ requirements on such a program. In both cases, machines implementing correct programs can still be said to miscompute.