> Type safety has nothing to do with software being more reliable or more secure.
It is true that type safety doesn't necessarily mean that software is more reliable and secure (it depends on the type system, the semantics of the language, and a host of other things), but saying it has "nothing" to do with it is incorrect. In particular, preventing undefined behavior certainly has an effect on security, whether or not it's through a static type system. As pcwalton has mentioned on several occasions, something like 50% of critical CVEs in Firefox exploited attack vectors that would have been prevented by Rust's type system.
This is where I disagree and believe that such way of thinking about bugs cannot take us anywhere.
Bugs have nothing to do with formal properties of the language. They are the result of people's thinking process. And type system may just as well be the thing someone was dealing with while making his next CVE-worthy mistake.
Factually, Rust's type system guarantees, if consistently upheld, would have eliminated those bugs. Empirically, we know that in typesafe languages like Java, these types of vulnerabilities are far less frequent. These are facts: you cannot "disagree" with them.
Even if we assume that people write buggy code at about the same rate in C++ and Rust, as long as the vast majority of Rust code is not inside an unsafe block, Rust still reaps this benefit, because bugs in safe Rust shouldn't cause memory unsafety.
Finally, yes, bugs do have something to do with formal properties of a language. Really. They do. You can prove that software matches its specification, or fulfills certain properties. People have. SeL4 is a thing. Relying on a static type checker means you only need to trust the static type checker to be correct in order to enforce the appropriate properties, not all code written in the language, and "the Rust type checker" is a much smaller kernel to trust, and will be more widely exercised and heavily scrutinized, than "all other Rust code ever written." This is literally the entire point of static type systems.
I apologize, but this is going to be my last response to you, because I don't think we can have a productive conversation about this.
> Factually, Rust's type system guarantees, if consistently upheld, would have eliminated those bugs.
You are missing my point. It doesn't guarantee to not cause other bugs. And saying that something eliminates some type of bugs is completely misleading, because this is not what matters. It matters to not cause other bugs as well as eliminate some bugs. Which is impossible to guarantee with formal methods. And which is why current academic approach to languages cannot bring us anything, until the whole system changes.
Psychological approach to programming language design is what has to happen. Anything else is broken.
It's impossible to eliminate all bugs, no matter what you do. Psychological design will eliminate some bugs but not all. Static type system will eliminate some bugs, but not all. The best you can do is try to eliminate as many bugs as possible, by doing multiple things that give the best returns, given the bugs you're targeting.
It is true that type safety doesn't necessarily mean that software is more reliable and secure (it depends on the type system, the semantics of the language, and a host of other things), but saying it has "nothing" to do with it is incorrect. In particular, preventing undefined behavior certainly has an effect on security, whether or not it's through a static type system. As pcwalton has mentioned on several occasions, something like 50% of critical CVEs in Firefox exploited attack vectors that would have been prevented by Rust's type system.