wrt. defunctionalization, another resource that requires only basic understanding of functional programming (lambdas and ADTs) and equational reasoning to understand it is lecture 4 of [0]. The procedure is quite straightforward if approached from a program derivation standpoint; first convert the program into CPS (see end of lecture 1). That is, solve the equation `progCont e k = k (prog e)` given prog. Then convert the closures into first-order structures by identifying the free variables they capture and deriving the closure-free version.

I really like Bartosz's blog post on defunctionalization and Freyd's theorem[1]. It's probably better to understand Freyd's theorem in the usual categorical presentation as Bartosz dualizes many things (because instead of a huge product of all environments we have a huge coproduct of possible environments, then select the "best"/"minimal" one using some universal cone as opposed to a maximal product).

Truly, defunctionalization is one of those things that can satisfy curiosity on many levels of abstraction from assembly to categories.

[0] http://www.cs.nott.ac.uk/~pszjlh/pcalc.html

[1] https://bartoszmilewski.com/2020/08/03/defunctionalization-a...