I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, and the Machines that represent the software which actually gets designed and implemented, say $M_\alpha$ and $M_\beta$, respectively.
Specifically, my interest is in examining limitations (due to Rice's Theorem for instance) in automated detection of errors in software programs between the Language processed by the ideal machine, and the language processed by the developed/implemented Machines.
Any reference to prior work that works with some notions of exploring differences between two specified Turing Machines, or barring that a lower level Formal Language would be extremely helpful and appreciated; because i'd rather cite than write :-).