Dependent types and totality

Whoever the fuck ever came up with the brilliant idea that all dependently-typed languages must be total? This is totally retarded, having to prove termination of everything. And it's totally unnecessary

Their only argument is "uh, you know, muh typechecking, it becomes undecidable". Guess what, dipshits, people have been running code whose termination is undecidable for decades. No one is afraid of non-terminating loops at runtime, so how can non-termination at compile-time be a problem? You run the typechecker, it crashes with an overflow/segfault/whatever, you edit your code and then it compiles. But nooo, these cretins believe that this is impossible and you have to only use total functions in types, and then prove that they terminate via structural recursion. Fucking academic numbskulls.

Now, of course totality is essential for proof assistants. But dependently typed languages are not all proof assistants! Dependently-typed languages can be Turing-complete with a Turing-complete, undecidable type system! Why don't these retards realize this?

if you can write an infinite loop in a language it will have a type like this f : forall a. Int -> a.

It is easy to prove anything you want from this, for example: f 3 : String = Int.

Now you can unsafeCoerce a String into an Integer causing malformed data.

That is why a dependently typed language should be total.