## ยง The dependently typed expression problem

Dependently typed programming is like the expression problem.
We can either write Ohad/OOP, where we have data and proofs (behaviour)
next to each other. Or we can write in Xavier/functional style, where
the data is separate from the proofs (behaviour).