Dependent types

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

>>21
all the Idris code does is force you to check if the divisor is 0, as if all division procedures in other languages don't already check if the divisor is zero. instead of crashing, in Idris you have, print "Attempt to divide by zero!", which is literally no different than catching the exception and doing that.

tl;dr the emperor has no clothes