Name: Anonymous 2015-02-01 22:27
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?
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?