Consider the scenario where my programme is dangerous for values of an unsigned integer less than or equal to 2. As far as I know, there is no such type for unsigned integers equal to 3 or more. Sure, in object oriented languages you can essentially define your own type, but this flexibility is where you are not protected against yourself.
I see your point about types though. That said, both types and testing exist to protect you. I stand by what I said, however; languages do not exist to protect you from yourself.
The usual idea is that while tests demonstrate the existence (and subsequent removal) of particular bugs only types (or proofs) show the non-existence of whole classes of bugs.
Such integer checks as you suggest are nothing more than a number paired with a proof that the number is less-than some bound. The properties of those proofs cannot be faked and their proper management and construction is all handled at compile time... Then erased.
I challenge you to write a red-black tree with the RB invariants exposed in the types and then continue to say languages do not exist to protect you from yourself. The moment these things end up in types the language starts to pull back on you.
Ada, and probably other languages, allows subtypes that restrict usage to a range of some other type. 2 sections below that is modular types, so you don't have to put in the `mod 500` or whatever your code needs every time, the compiler will fill that in for you as long as you are using that type.
> Consider the scenario where my programme is dangerous for values of an unsigned integer less than or equal to 2. As far as I know, there is no such type for unsigned integers equal to 3 or more. Sure, in object oriented languages you can essentially define your own type, but this flexibility is where you are not protected against yourself.
You can specify that type in a dependently typed language. Then, if you can prove that values of that type can not violate your requirement, there is no runtime overhead.
Are there things which are unknowable or unprovable in a dependently typed system? Sure. But I think your initial assertion that all languages are unsafe to a degree and therefore it can't be their job to protect you against mistakes is unhelpful; it muddies the water by appealing to the fact that 'nothing is perfect/no approach is perfect'. But the whole point with type systems is to eliminate certain classes of bugs - the rest can hopefully be caught by other, less rigorous means, like fuzzy testing and unit testing. All other bugs are relegated to problems which are (in general) undecidable.
I think there is an important and quite general point here: it is not just about programming languages, but also about programming knowledge and skills. You are replying to someone who was unaware of the state of the art in program verification (to be fair, he recognized the issue to be solved, which is an important start.)
As the example in the original post demonstrates, programming in languages that have this level of support for verification is very different from programming as it is currently commonly practiced. Not everyone will be capable of making the switch, and for an organization to simply say 'from now on, we are going to use this safe language', without addressing the skills issue, is setting up for failure.
> I think there is an important and quite general point here: it is not just about programming languages, but also about programming knowledge and skills. You are replying to someone who was unaware of the state of the art in program verification (to be fair, he recognized the issue to be solved, which is an important start.)
Well let me be clear that I knew of program verification because I'm a PL geek, not because of any skill whatsoever.
> Not everyone will be capable of making the switch, and for an organization to simply say 'from now on, we are going to use this safe language', without addressing the skills issue, is setting up for failure.
Well, let's keep the discussion to programmers who really need the things that we are after - safety and efficiency. It's not all programmers, just programmers in some domains. Some people might even think that some people can't adjust to writing low-level code ala C, period. But some domains need these things, which means that we just need the programmers who are motivated enough/have the patience to learn it. Just those programmers, not all programmers.
If we can't get them, then maybe some one will actually have to offer some incentives like money - instead of a purely volunteer effort as I think was the case in this debacle. :)
I wasn't intending to cast doubts on any particular individual's skills, which is why I wrote 'knowledge and skills'. I am learning this stuff myself.
You make some good points about where safety matters most, but I think a greater general awareness would help drive adoption where it matters. Furthermore, while this problem had widespread consequences due to it being in widely-deployed system- or middle-level software, 'ordinary' programming can have quite serious vulnerabilities, too.
I think schools, especially below the first tier, could do more to promote awareness of static verification and other safe practices, and that might modify the way their graduates approach development, even though they probably will not be using formal methods.
There are things that can be done to improve safety in general-purpose programming languages. I feel certain that garbage collection and the avoidance of pointers has made programming safer, but I suspect 'duck' typing has had the opposite effect.
In the past, the DOD has been a driver of code safety, though it has backed down from its possibly ill-advised 'nothing but Ada' position. In fact, Ada might be the counter-example to the idea that you can drive safety through language choice.
You would think the banks would have a vested interest in improving things. Perhaps they could divert a fraction of their bonus payments to create incentives...
I see your point about types though. That said, both types and testing exist to protect you. I stand by what I said, however; languages do not exist to protect you from yourself.