Dependent types

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

Someone explain to me how the fuck you can check bounds purely at compile time. Let's say the array is user input. Yeah good luck buddy. You're still going to have a conditional branch in the machine code.