He talked about Agda2. My experience using advanced type system tells me that you can get away with functional tests. Types, also, takes much less code space-p

He talked about Agda2. My experience using advanced type system tells me that you can get away with functional tests. Types, also, takes much less code space-programmer's time than tests. So I do not see how they could be harder to use. Certainly types will be unusual, but not much harder.