OCaml developers at Tezos often use fold_left function
in the code. Maybe the reason is that it is a bit easier to write efficient
code using fold_left than fold_right.
fold_left and fold_right from OCaml library: List
val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.
val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)).
Not tail-recursive.
And from formal verification point of view,
it is much easier to prove statements about fold_right either than about fold_left.
Why? The reason is in how these functions are organized. Formal verification often uses
mathematical induction as an instrument for proving statements on the lists.