Can we extend this to more properties, such as: Does IO, makes system calls, launches or interacts with threads, may block or has an unexpected space/time complexity?

Kind of, via effects, which is yet another way to use the type system to enforce specific kinds of execution flows.