It might depend on the problem space. I dunno. But I suspect it depends a lot on the type system and type inferencer of the language you use. It is easier to w

It might depend on the problem space. I dunno. But I suspect it depends a lot on the type system and type inferencer of the language you use. It is easier to write a true statement than it is to prove the statement is true, and getting a compiler to agree to compile quite literally requires proving a statement is true. This can be more or less difficult based on the language. I’ve read a lot of war stories, particularly in java, about having to do a lot of crazy convoluted code to get the compiler to realize that yes actually these 2 objects are interchangeable from an API/Interface point of view. I don’t know, but I suspect this may be a lot less common in languanges using hindley-milner type system, since that lends itself to very good type inferencing.