One being the idea of types as describing shape of data. In the best of cases perhaps some semantics tied to the data (how the bits are to be interpreted)
Than there is the the other view, the Curry-Howard one. Where types describes proofs and invariants of the program it self, and how interesting properties of program compositions can be ensured.
It seems much time is wasted when people holding one perspective debates with people holding the other.
Perhaps we should have separate words for these concepts.
One being the idea of types as describing shape of data. In the best of cases perhaps some semantics tied to the data (how the bits are to be interpreted)
Than there is the the other view, the Curry-Howard one. Where types describes proofs and invariants of the program it self, and how interesting properties of program compositions can be ensured.
It seems much time is wasted when people holding one perspective debates with people holding the other.
Perhaps we should have separate words for these concepts.