An expressive and ergonomic type system goes a very long way into codifying that intent.

For example, it's quite obvious what the intent of this Idris function is: `f : Vect n (Vect m a) -> Vect m (Vect n a)` (where `Vect` is the type of lists of a given length).