Programmers use it all the time! They turn diagrams representing the logic of the business domain into expressions in their type system of choice. I think it’

Programmers use it all the time! They turn diagrams representing the logic of the business domain into expressions in their type system of choice. I think it’s a failure of pedagogy to focus on the abstract “prove stuff” sense, rather than the applied “domain diagram logic to types” at the core of what SDEs actually do. But turning a business domain diagram into a systems diagram into code is translating a category into another via embedding before translating into a type theory. My opinion is that you need to start with that core and explain how the other features make that better, eg, how does polynomial monads address the weirdness between logging and errors (and errors in logging errors, etc)?