An absolute not to be missed lecture by David Sankel: The intellectual Ascent to Agda.

He talks about Denotational Semantic and interestingly describing it as:  augmenting math to talk about meaning and then extend math to program in math.