Program differences are pervasive in software development, but most of the
time they are represented as textual differences with no regards to the
syntactic nature of programming languages or their semantics. Thus, they may
be hard to read and often fail to convey insight on the changes on
semantics. Furthermore, such low-level, unstructured presentations are hard to
reason about.

We present a formal framework to characterize differences between
deterministic programs in terms of their small-step semantics. This
language-agnostic framework defines the notion of /difference languages/ in
which /oracles/—programs that relate small-step executions of pairs of program
written in a same language—can be written, reasoned about and composed.

We illustrate this framework by instantiating it on a toy imperative language
and by presenting several /difference languages/ ranging from trivial
equivalence-preserving syntactic transformations to characterized semantic
differences. Through those examples, we will present the basis of our
framework, show how to use it to relate syntactic changes with their effect on
semantics, how one can abstract away from the small-step semantics
presentation, and discuss the composability of oracles.

This is joint work with Thibaut Girka (IRIF - MERCE) and David Mentré (MERCE)