A programmer hears that she needs to create a function that adds up all the numbers in a list of numbers. The programmer identifies that this is a good situation for using the built in library function List.fold_left, and so does this.
However, where does she get this knowledge that a fold is the correct function to call. She hears the problem and recognizes that this problem has the pattern of accumulating the data into an accumulator, knows that fold often fits the pattern of accumulating data, and fills in the data so that it typechecks and performs the correct action; 0 for empty list and (+) for accumulation.
How could we inform the computer that it needs to perform that accumulation action, and know that fold is appropriate.
We first need to have formalized what the notion of accumulate is. Certainly the definition of fold formalizes it. The implementation of fold is shown below.
let rec fold_left (f:'a->'b->'a) (acc:'a) (l : 'b list) : 'a =
begin match l with
|  -> acc
| h::t -> fold_left f (f acc x) xs
This feels too specific for an specification for something that accumulates. I can’t however find anything more general. This is a difficulty in trying to encode semantics, in that the semantics seem to become as complicated as the program. Perhaps not a complete specification is correct, but to give invariants that imply, or nearly imply, the complete semantics of the program is sufficient. For example, instead of writing out exactly what we want the accumulator to handle, we want to know that sum (l:’a list) has properties that sum  = 0 and sum (h::t) = h+sum(t). This is certainly more specific than merely int list -> int, but not yet a full implementation. However, it seems to give enough information to provide a full implementation, and there is a natural way to extend the specification to an implementation. Perhaps allowing for a stronger type system will enable more instances where the type informs the implementation in immediate ways.