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