> That's the thing though, the "social problems" are the important problems.
And yet, we still seem bogged down with bugs and vulnerabilities caused by non-social problems. So use types to get rid of those problems, and then we can worry about the social problems.
> Lack of strong typing does not seem to be the issue. Lacking domain understanding/logical errors is the problem.
Types help with this too. Formalizing a property that is inconsistent, underspecified, or over-constrained is a natural part of designing a type to represent that property.
So formalizing things with type systems is great. In fact, I'm a huge proponent of it.
The problem still remains, you may not have a sufficiently well developed requirement set to be able to specify things in your type system.
I'll give an example: It's possible in Haskell (really many languages) to create a type SafeString which can be constructed from a standard String and does all the necessary escaping for the target (let's say it takes in a username and works to prevent sql injection attempts, or removes HTML tags, or whatever might be appropriate). And for all practical purposes it behaves exactly like a string otherwise. Any time you want to make a SQL query or generate some HTML you know that you can use a SafeString and it'll (barring errors in implementation) work without causing you either security risks or producing incorrect outputs.
That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this.
The type system itself doesn't tell you that your types are underspecified. It needs to come from the requirements analysis (in this case, requirements as viewed through a security-oriented perspective). But type systems allow you to encode that specification once it's been made.
> That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this. The type system itself doesn't tell you that your types are underspecified.
Indeed type checking alone won't tell you that, but my point was more that type-driven design has a much better chance at revealing such underspecified requirements.
If you resist the urge to be lazy by assuming that your domain types map perfectly to built-in types, like String or Int32, and instead assume that your domain needs its own types, you centralize the validation logic to create domain types, which can then be easily audited and tested.
So you should create a distinct SafeString or SqlQuery type as a natural part of modelling your domain, even if the semantics of String appear sufficient.
And yet, we still seem bogged down with bugs and vulnerabilities caused by non-social problems. So use types to get rid of those problems, and then we can worry about the social problems.
> Lack of strong typing does not seem to be the issue. Lacking domain understanding/logical errors is the problem.
Types help with this too. Formalizing a property that is inconsistent, underspecified, or over-constrained is a natural part of designing a type to represent that property.