In a way, type-systems are less powerful non-turing-complete languages that are guaranteed to halt, thus can be checked at compile-time.

I think we need powerful but easy-to-restrict languages. Can you mark that function as pure, as not safe? that kind of thing.