[Laaas]

In practice, all simple behaviour you want can be expressed succinctly. If you want it to have complex behaviour, the type is complex. This is no different from using natural language to describe the problem. If for example we want it to implement multiplication, how would we do that? We'd operate not on built-in integers (which have the operation already), but e.g. on an explicit list of bits. Let's make the list length indexed. We get `mult : Vec n Bool -> Vec m Bool -> Vec (n + m) Bool` This is not enough to constrain it. We add `mult 1 n = n`, `mult n m = mult m n`, `mult 0 n = 0`, `mult n (mult m o) = mult (mult n m) o`, and finally, `mult n (add m o) = add (mult n m) (mult n o)`. This uniquely characterises multiplication on the natural numbers.

In natural language, it might suffice to say "implement multiplication", but this is because it _knows_ what multiplication is beforehand. If it did not, and only knew how to code, you would effectively have to restate the exact same properties. This will more often be the case when you're not dealing with trivial examples.