The semantics of logics is based on valuations that map variables to values, while programming languages cannot store complex values atomically. They have a pointer semantics where complex data is stored on the heap, linked with pointers. The standard approach to bridge the semantic gap between algebraic specifications and executable programs is to translate algebraic data types, recursive definitions and programs to functional code with immutable data types. Since functional programs are often less efficient than C programs due to the lack (or limited use) of mutation and the requirement of using garbage collection, we develop a different approach in this paper that is based on always mutating data structures but keeping different ones disjoint. The approach generates efficient C programs from the specifications, which have a pointer semantics and explicitly allocate and free memory on the heap. Formal specifications are given for the semantics of a core source and target language that allow to demonstrate the main transformations necessary and prove their correctness. The approach has been implemented for the full language and produces working C code.