A formal specification of an algorithm is a very rich mathematical abstraction. In general, it not only specifies an input-output relation, but also - at some level of abstraction - constrains the states and transitions associated with computing this relation. This paper explores the relationship between a formal specification of an algorithm and the many different ways in which the associated states and transitions can be embodied in physical objects and agency. It illustrates the application of principles, tools and techniques that have been developed in the Empirical Modelling Project at Warwick and considers how such an approach can be used in conjunction with a formal specification for exploration and interpretation of a subject area. As a specific example, we consider how Empirical Modelling can be helpful in gaining an understanding of a formal development of a heapsort algorithm.