3 ms·
> But it has now taken a new interpretation in the last couple of decades: Static typing is a form of compile-time error checking, so it will help you produce b
by Blikkentrekker 6y ago
> But it has now taken a new interpretation in the last couple of decades: Static typing is a form of compile-time error checking, so it will help you produce better quality code. It is as if static typing is a magical theorem prover that will verify some deep properties of your program. This is where I call bullsh*t.[sic] I have never had a static type checker (regardless of how sophisticated it is) help me prevent anything more than an obvious error (which should be caught in testing anyway).
That's an anecdote; facts are that serious critical bugs that lead to privilege escalation and loss of data have existed in codebases that would surely have been caught by various static type systems.
> In other words, static typing is pointless. It has, maybe, some documentary value, but it does not substitute documentation on other invariants. For example, your invariant might be something like I’m expecting here a monotonically increasing array of numbers with a mean value of such and such and a standard deviation of such and such. The best any static type checking will let you do is “array[float]”. The rest of your invariant must be expressed in words as a documentation of that function. So why subject yourself to the misery of “array[float]”?
With dependent typing, it's actually quite possible to both define a type for “sorted list” and prove to the type checker that a sorting algorithm does sort it.
- didibus 6y ago> That's an anecdote; facts are that serious critical bugs that lead to privilege escalation and loss of data have existed in codebases that would surely have been caught by various static type systems. An anecdote at this point is at least better than a baseless claim as you're making. Also keep in mind the article is in the context of Lisp, so it would be static types on top of a garbage collected memory managed runtime with runtime type checks.
- kazinator 6y ago> That's an anecdote; facts are that serious critical bugs that lead to privilege escalation and loss of data have existed in codebases that would surely have been caught by various static type systems. Do you have any non-strawman examples of this (e.g. C security holes are strawman).
- AnimalMuppet 6y agoGiven who you are, I'm going to give you the benefit of the doubt, but... What? C security holes are strawman? What is your basis for saying so?
- kazinator 6y agoFirstly, C is statically typed, so if you're arguing for static typing as the cure for security holes, citing C examples of security hoes won't speak well for your argument Secondly, C has an incomplete static system, which has no run-time safety net to compensate for it. Many properties of C programs go unchecked. What is checked is easily defeated with type casts. Even the numeric conversions lack safety; e.g. floating point to integer conversion is silently implicit, with undefined behavior if the value is out of range. All of that is a straw man example if we are arguing against incomplete static type systems, because the iron man is incomplete static with strong dynamic checks. C also doesn't provide access to the language at compile time; we cannot execute test cases for the code in the same breath as compiling it. If code is cross-compiled, it needs unit tests compiled into individual executable programs, and an emulator like QEMU to run them. Because C doesn't have run-time safety, unit tests do not reliably flush out type errors; programs with type errors can pass unit tests by fluke due to undefined behavior. E.g. a string that is not properly null terminated can have a zero byte in the right place anyway during the execution of a test case, and so on. C security holes are not a good example to invoke in a static/dynamic debate as something that could be prevented with static, so I'm asking that: if those are the examples, please spare the debate.
- AnimalMuppet 6y agoOK, now I understand your point. C's static type system is inadequate to prevent C's security issues - that's kind of self-evident, when you put it that way. [Edit: More precisely, C's type system is inadequate to prevent the kinds of security errors common in C code.] What's your stance on a stronger static type system being able to prevent them?
- deleted 6y ago