Abstract data type as an algebra

Summary

In the algebraic approach to programming, an abstract data type is described by its operations and their equations. It does not depend on a concrete memory layout. Such a description is an algebraic specification: a many-sorted signature together with a set of equations. The data type itself is the initial algebra of the specification, which is unique up to isomorphism. So any two correct implementations behave in the same way. This view, worked out in the 1970s, makes the correctness of an implementation a question about homomorphisms of algebras.