Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

There’s no way you can encode all the logic to sanitize input in just types.

B-b-but you can write code that output types!

But I can also directly write that code without types as a middleman.