The specifications are written in ML. Although executable, the specifications are intended to describe the desired results of the calculation, not necessarily the way the calculation should be done. Therefore, the specification should not be taken as a description of a desired algorithm. In some cases, the specification is an inefficient way of computing the results.