> > It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so
> This is where the argument became circular and we can basically stop.
I think any appeal to "easier" is inherently subjective. I've certainly tried to avoid making any such claims. Instead, I've mostly tried to argue that static types can forbid certain programs from ever running, and we can use that to forbid things like vulnerable SQL queries.
> > It's possible to implement anything correctly with dynamic types
> but apparently chriswarbo does not.
I never said any such thing; besides which, it's trivially the case that anything implemented with static types could also be implemented with dynamic types, since static types only exist at compile time (they are "erased" during compilation), and hence every running program is dynamically typed.
In fact, I don't think I've said anything about correct implementations at all. My point is that static types can forbid incorrect implementations. When it comes to security, that is much more important; i.e. I would much rather bang my head against a screen filled with compiler errors, than expose some insecure program to the harsh reality of the Internet.
> The parent claim (by chriswarbo) was that, for example, SQL injection attacks were, in fact, incontrovertible proof that SQL injection attacks "are classic type errors".
I've not claimed that (in fact, I'm stuggling to parse what that sentence might even mean). I claim that SQL injection attacks are "classic type errors" in the sense that:
- It's a widespread problem, easily encountered, commonly warned about, and most developers have probably done it at some point.
- It's a class of error that can be entirely ruled out at the language/API level, through use of static types. Similar to how segfaults can be entirely ruled out at the language level, using managed memory like in Python/JS/etc.
- Due to the above, it's a common example used to illustrate the usefulness of static types in blog posts, articles, etc. One which sticks in my mind is "A type-based solution to the “strings problem”: a fitting end to XSS and SQL-injection holes?" https://blog.moertel.com/posts/2006-10-18-a-type-based-solut...
- Due to the above, it's considered "folk wisdom" (or a "folk theorem") in the relevant fields (e.g. Programming Language Theory, Formal Methods, etc.)
Other examples of "classic type errors" might include:
- Mixing up integers with strings-of-digits, e.g. 'print("You were born around " + (time.now.year - input("How old are you?"))'
- Forgetting to 'unwrap' some list element, e.g. 'open(listdir("config/")).read()' instead of 'listdir("config/").map(f => open(f).read())'
- Mixing up units of measure, e.g. 'distance = speed + time' instead of 'distance = speed * time'
Basically any common mix-up between values/components in a program, where the computer could help up to spot the mix-up (perhaps entirely automatically, if type inference is involved). In the case of SQL injection, the mix-up is between 'string of bytes' and 'SQL query'.
> And yes, that article is somewhat old, but the evidentiary situation has not changed, despite further attempts to make the claim that static typing is provably better. Claims that were resoundingly debunked.
I very much appreciate when researchers attempt to ground things in a bit more empiricism! Unfortunately those particular studies just aren't looking at the sorts of things that I find relevant; in particular, those studies (and that linked blog post, and many of the comments here), seem overly-preoccupied with mundane trivialities like "string", or "int", or "SQLColumnName".
Personally, I'm much more interested in how types can help me:
> It's a class of error that can be entirely ruled out at the language/API level, through use of static types.
Repeating this claim doesn't make it true.
Once again: this has nothing to do with static vs. dynamic types, and everything to do with modelling.
To make this clear, let's compare a dynamically and a statically type-checked version of this with the model of SQL as just strings.
Both the dynamically and the statically type-checked version of this program will be susceptible to SQL injection attacks. The statically type-checked version will verify at compile time that all the values are indeed strings.
Now let's compare a dynamically and a statically checked program with a proper model for the SQL, not strings.
Both of these will not be susceptible to SQL injection attacks.
It has nothing to do with static vs. dynamic, and everything with how you model the problem.
> This is where the argument became circular and we can basically stop.
I think any appeal to "easier" is inherently subjective. I've certainly tried to avoid making any such claims. Instead, I've mostly tried to argue that static types can forbid certain programs from ever running, and we can use that to forbid things like vulnerable SQL queries.
> > It's possible to implement anything correctly with dynamic types
> but apparently chriswarbo does not.
I never said any such thing; besides which, it's trivially the case that anything implemented with static types could also be implemented with dynamic types, since static types only exist at compile time (they are "erased" during compilation), and hence every running program is dynamically typed.
In fact, I don't think I've said anything about correct implementations at all. My point is that static types can forbid incorrect implementations. When it comes to security, that is much more important; i.e. I would much rather bang my head against a screen filled with compiler errors, than expose some insecure program to the harsh reality of the Internet.
> The parent claim (by chriswarbo) was that, for example, SQL injection attacks were, in fact, incontrovertible proof that SQL injection attacks "are classic type errors".
I've not claimed that (in fact, I'm stuggling to parse what that sentence might even mean). I claim that SQL injection attacks are "classic type errors" in the sense that:
- It's a widespread problem, easily encountered, commonly warned about, and most developers have probably done it at some point.
- It's a class of error that can be entirely ruled out at the language/API level, through use of static types. Similar to how segfaults can be entirely ruled out at the language level, using managed memory like in Python/JS/etc.
- Due to the above, it's a common example used to illustrate the usefulness of static types in blog posts, articles, etc. One which sticks in my mind is "A type-based solution to the “strings problem”: a fitting end to XSS and SQL-injection holes?" https://blog.moertel.com/posts/2006-10-18-a-type-based-solut...
- Due to the above, it's considered "folk wisdom" (or a "folk theorem") in the relevant fields (e.g. Programming Language Theory, Formal Methods, etc.)
Other examples of "classic type errors" might include:
- Mixing up integers with strings-of-digits, e.g. 'print("You were born around " + (time.now.year - input("How old are you?"))'
- Forgetting to 'unwrap' some list element, e.g. 'open(listdir("config/")).read()' instead of 'listdir("config/").map(f => open(f).read())'
- Mixing up units of measure, e.g. 'distance = speed + time' instead of 'distance = speed * time'
Basically any common mix-up between values/components in a program, where the computer could help up to spot the mix-up (perhaps entirely automatically, if type inference is involved). In the case of SQL injection, the mix-up is between 'string of bytes' and 'SQL query'.
> And yes, that article is somewhat old, but the evidentiary situation has not changed, despite further attempts to make the claim that static typing is provably better. Claims that were resoundingly debunked.
I very much appreciate when researchers attempt to ground things in a bit more empiricism! Unfortunately those particular studies just aren't looking at the sorts of things that I find relevant; in particular, those studies (and that linked blog post, and many of the comments here), seem overly-preoccupied with mundane trivialities like "string", or "int", or "SQLColumnName".
Personally, I'm much more interested in how types can help me:
- Avoid leaking secret information https://link.springer.com/chapter/10.1007/978-3-030-17138-4_...
- Guarantee big-O resource usage https://twanvl.nl/blog/agda/sorting#a-monad-for-keeping-trac...
- Guarantee the correct order of operations https://docs.idris-lang.org/en/latest/st/machines.html
- Prevent AI agents from losing capabilities http://chriswarbo.net/projects/powerplay