The language Esterel is designed for safety-critical reactive applications and has been used, for example, in the maintenance and test computer, landing gear control computer, and virtual display systems of civilian and military aircraft at Dassault Aviation (Berry et al. 2000) and the specification of part of Texas Instrument’s digital signal processors (Benveniste et al. 2002). Esterel’s success stems from its ability to express complex control decisions that require both concurrency and determinism. Esterel is designed to be embedded into a host language, augmenting the host with these features. This setup is so inherent that Pure Esterel does not come equipped with its own notions of values, or of expressions that compute values: it has only terms that describe control flow and concurrency. The notion of value is borrowed from the host language. Esterel’s unusual semantics and use in safety-critical systems has lead to its semantics being well studied (Benveniste and Berry 1991; Berry 2002; Berry and Gonthier 1992; Berry et al. 1993; Florence et al. 2019; Potop-Butucaru 2002; Potop-Butucaru et al. 2007; Tardieu 2007; Tini 2001). However none of these fully capture Esterels symbiotic nature while still allowing for understanding and analysis of fragments of programs at a syntactic level. As a step towards closing this gap I am attempting to prove that contextual equivalence between Pure Esterel1 terms is preserved and reflected by its compilation to circuits: that is that the Esterel compiler is fully abstract. This will be a stepping stone to developing further semantics which can reason about Esterel and its Host language together. I will do this by proving that the calculus for Esterel (Florence et al. 2019) is sound and adequate with respect to the circuit translation from Esterel (Berry 2002). Then I will use calculus to derive a decision procedure for contextual equivalence, which proves fully abstract compilation. The remainder of this document gives an informal explanation of a fragment of Esterel (section 1), a discussion of the kinds of circuits Esterel compiles into (section 2) and a description of my plan for proving fully abstract compilation and the work so far (section 3).