§ 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).