Program state visualizations (PSVs) help programmers understand hidden program state like objects, references, and closures. Unfortunately, existing PSV tools do not support custom language semantics, which educators often use to introduce programming languages gradually. They also fail to visualize key pieces of program state, which can lead to incorrect and confusing visualizations.

Theia, a generic PSV framework, uses formal abstract machine definitions to produce complete, continuous, and consistent (CCC) PSVs.

To produce CCC visualizations with Theia, an educator only needs to specify an abstract machine and optionally customize the resulting web page, allowing her to visualize custom language semantics without developing a language-specific tool. We explain how Theia’s design produces CCC PSVs by construction with a series of case studies based on a functional and an imperative language.

Theia’s design is guided by the existing, but underappreciated, insight that formalized notional machines are abstract machines. We describe research questions and opportunities in Programming Languages (PL) and Computer Science Education Research (CER) that result from this observation.