3 ms·

> 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 ci

> 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. 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". That simply isn't true, at least not in the sense of static type checking (and only made true, as I mentioned above, by conflating "static type", "type" and "model" into one incoherent gooey mush). chriswarbo's incorrect claim was in response to my referenced article, The Safyness of Static Typing [1], where I (as a prelude to my actual point) look at the evidence for the claim that "static types make it easier to implement something correctly". There isn't any. Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. 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. So that's the background. With this background we have the idea that SQL injection attacks are somehow evidence for the problems with dynamic typing, which they are not. I can have a statically checked string type and have exactly the same SQL injection attacks, and in principle, checking code needs to run at runtime against the dynamic input it is represented with. Which I think we agree on: > It's possible to implement anything correctly with dynamic types but apparently chriswarbo does not. So that brings us to the circularity of the argument: > but the point is static typing makes it easier to do so This hasn't been shown. It was claimed. And it was claimed that SQL injection somehow proves this. Which it doesn't, because we agree that what prevents the attack is the code that runs, the model that executes. It may be that such code is easier to write with static types, but that hasn't been shown, it is just claimed and the claim repeated in support of the claim. Circle. [1] https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t...

seanwilson 5y ago
> Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. You mean the link from [1] to "An experiment about static and dynamic type systems" based on "an empirical study with 49 [undergraduate] subjects that studies the impact of a static type system for the development of a parser over 27 hours working time.". I think studies like this are more distracting here than useful (low skill level, not large scale enough, too much noise, toy example). The article here sums up a lot of my thoughts on this: https://news.ycombinator.com/item?id=27892615 https://news.ycombinator.com/item?id=27892615 And do you really need a study that proves e.g. (to pick a simpler example to summarise) a language that makes it impossible for null deferences to happen at compile-time is going to have less null dereference errors than one that lets those errors happen at runtime? It's like insisting for an empirical study that 2 + 2 = 4. > It may be that such code is easier to write with static types, but that hasn't been shown, The typed SQL example might look something like: function getUserInput(): string function createSanitisedString(s: string): SanitisedString function createSafeSqlQuery(s: SanitisedString): SqlQuery For the code `createSafeSqlQuery(getUserInput())`, a static type checker would stop the entire program from starting with a type error pinpointing the exact line where the unsanitised data is coming from. With a dynamic type checker: 1. At best, the code will fail only after the user input is received by createSafeSqlQuery during runtime and you won't know where the input originated from. 2. At worst, the coder forgets to add a check like `typeof s === SanitisedString` or a call to `createSanitisedString` in `createSafeSqlQuery` and creates an injection attack. The static type checker clearly wins here for me for safety and ease of implementing correctly. I don't need a study to know that compile-time errors are better than production runtime errors, that automated and exhaustive checks of correctness are better than the coder having to remember to add manual checks, and that it's better to know the exact line the unsanitised input came from over only knowing it comes from somewhere. What languages have you used that have strong static type systems that you've written large programs in? Have you tried OCaml or Haskell for example?
- simiones 5y ago
  > function createSanitisedString(s: string): SanitisedString > function createSafeSqlQuery(s: SanitisedString): SqlQuery The problem with the whole argument is that these functions are not actually enough to work with SQL, since they don't allow us to create dynamic SQL from safe strings. Here are some ideas of why we can' use the functions you proposed: user_filter = raw_user_input_col_name ++ " LIKE ?" createSafeSQLQuery("SELECT * FROM my_table WHERE " ++ user_filter ++ ";") //type error sanitizedQuery = createSanitisedString("SELECT * FROM my_table WHERE" ++ user_filter ++ ";") //should return error or quote everything createSafeSQLQuery("SELECT * FROM my_table WHERE" ++ createSanitisedString(user_filter) ++ ";") //filter will be wrong, type error Let's now add something to allow us to achieve our goal: function asSanitizedString(s: string) : SanitizedString { return s } user_filter = createSanitizedString(raw_user_input_col_name ) ++ asSanitizedString(" LIKE ?") query = asSanitizedString("SELECT * FROM my_table WHERE") ++ user_filter ++ asSanitizedString(";") createSafeSqlQuery(query) //works, nice createSafeSqlQuery(asSanitizedString("SELECT * FROM my_table WHERE " ++ user_col_name ++ "LIKE ?;")) //oops, this also works You can achieve all of this with a non-string API: you can have an SQL DSL or just an SQL AST library; or you can use an ORM. But either way, you can't fix it without modeling the entirety of SQL into your type system (or as much of SQL as you are willing to support). If you don't believe me, go looking for a library that allows arbitrary strings as SQL, but statically ensures user input can't be used to construct an SQL query. I don't know of any one.
  - seanwilson 5y ago
    > The problem with the whole argument is that these functions are not actually enough to work with SQL My bad for being unclear but I meant you would be sanitising something like the user entering "tea cups" into a shop search input form and searching your shop product database with that. I didn't mean the user would be entering SQL queries. > But either way, you can't fix it without modeling the entirety of SQL into your type system Using the type system to check correctness sounds good to me. This is getting way too into the weeds about SQL anyway. Null dereference checks are a less distracting example to focus on for instance. As long as you can encode it into the type system, all my points are still relevant.
chriswarbo 5y ago
> > 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-solution-to-the-strings-problem.html 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_3 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-track-of-the-runtime 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 https://docs.idris-lang.org/en/latest/st/machines.html - Prevent AI agents from losing capabilities http://chriswarbo.net/projects/powerplay http://chriswarbo.net/projects/powerplay

seanwilson 5y ago

> Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. You mean the link from [1] to "An experiment about static and dynamic type systems" based on "an empirical study with 49 [undergraduate] subjects that studies the impact of a static type system for the development of a parser over 27 hours working time.". I think studies like this are more distracting here than useful (low skill level, not large scale enough, too much noise, toy example). The article here sums up a lot of my thoughts on this: https://news.ycombinator.com/item?id=27892615 https://news.ycombinator.com/item?id=27892615 And do you really need a study that proves e.g. (to pick a simpler example to summarise) a language that makes it impossible for null deferences to happen at compile-time is going to have less null dereference errors than one that lets those errors happen at runtime? It's like insisting for an empirical study that 2 + 2 = 4. > It may be that such code is easier to write with static types, but that hasn't been shown, The typed SQL example might look something like: function getUserInput(): string function createSanitisedString(s: string): SanitisedString function createSafeSqlQuery(s: SanitisedString): SqlQuery For the code `createSafeSqlQuery(getUserInput())`, a static type checker would stop the entire program from starting with a type error pinpointing the exact line where the unsanitised data is coming from. With a dynamic type checker: 1. At best, the code will fail only after the user input is received by createSafeSqlQuery during runtime and you won't know where the input originated from. 2. At worst, the coder forgets to add a check like `typeof s === SanitisedString` or a call to `createSanitisedString` in `createSafeSqlQuery` and creates an injection attack. The static type checker clearly wins here for me for safety and ease of implementing correctly. I don't need a study to know that compile-time errors are better than production runtime errors, that automated and exhaustive checks of correctness are better than the coder having to remember to add manual checks, and that it's better to know the exact line the unsanitised input came from over only knowing it comes from somewhere. What languages have you used that have strong static type systems that you've written large programs in? Have you tried OCaml or Haskell for example?

simiones 5y ago
> function createSanitisedString(s: string): SanitisedString > function createSafeSqlQuery(s: SanitisedString): SqlQuery The problem with the whole argument is that these functions are not actually enough to work with SQL, since they don't allow us to create dynamic SQL from safe strings. Here are some ideas of why we can' use the functions you proposed: user_filter = raw_user_input_col_name ++ " LIKE ?" createSafeSQLQuery("SELECT * FROM my_table WHERE " ++ user_filter ++ ";") //type error sanitizedQuery = createSanitisedString("SELECT * FROM my_table WHERE" ++ user_filter ++ ";") //should return error or quote everything createSafeSQLQuery("SELECT * FROM my_table WHERE" ++ createSanitisedString(user_filter) ++ ";") //filter will be wrong, type error Let's now add something to allow us to achieve our goal: function asSanitizedString(s: string) : SanitizedString { return s } user_filter = createSanitizedString(raw_user_input_col_name ) ++ asSanitizedString(" LIKE ?") query = asSanitizedString("SELECT * FROM my_table WHERE") ++ user_filter ++ asSanitizedString(";") createSafeSqlQuery(query) //works, nice createSafeSqlQuery(asSanitizedString("SELECT * FROM my_table WHERE " ++ user_col_name ++ "LIKE ?;")) //oops, this also works You can achieve all of this with a non-string API: you can have an SQL DSL or just an SQL AST library; or you can use an ORM. But either way, you can't fix it without modeling the entirety of SQL into your type system (or as much of SQL as you are willing to support). If you don't believe me, go looking for a library that allows arbitrary strings as SQL, but statically ensures user input can't be used to construct an SQL query. I don't know of any one.
- seanwilson 5y ago
  > The problem with the whole argument is that these functions are not actually enough to work with SQL My bad for being unclear but I meant you would be sanitising something like the user entering "tea cups" into a shop search input form and searching your shop product database with that. I didn't mean the user would be entering SQL queries. > But either way, you can't fix it without modeling the entirety of SQL into your type system Using the type system to check correctness sounds good to me. This is getting way too into the weeds about SQL anyway. Null dereference checks are a less distracting example to focus on for instance. As long as you can encode it into the type system, all my points are still relevant.

chriswarbo 5y ago

> > 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-solution-to-the-strings-problem.html 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_3 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-track-of-the-runtime 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 https://docs.idris-lang.org/en/latest/st/machines.html - Prevent AI agents from losing capabilities http://chriswarbo.net/projects/powerplay http://chriswarbo.net/projects/powerplay