This paper examines different ways to represent and validate core program
transformations. As the leading exemple, we take finite differencing, and
subject it to alternative encodings. Our first encoding is to represent
finite differencing equationally, and appeal to rewrite based
simplification to apply it. The second encoding is to represent the
transformation as a library refinement and use diagram pushouts to apply
it. Finally we consider an encoding as a metaprogram that works on the
abstract syntax tree of Specware terms. While metaprogramming allows
finegrained contro over the transformations it may be less declarative than
object level axiomatization, and often less transparent.  The assurrance
problem for meta-programs becomes an issue when having to rely on a
dinamically growing set of transformations, in a fastly moving scenario.
While this can be recast as a compiler correctness problem, we shall
discuss type based partial correctness criteria, an even mre interestingly,
frameworks for automatic inference of meta-typeability: the meta programs
transform well typed programs into well typed programs.