Comment by spoiler

What are the efficient ways of preventing this kind of bug, if not type systems?

The parent had a good point and you should really try to look at Haskell before you say that kind of nonsense.

All the tools that are available for static analysis are basically extra type systems bolted on top of existing languages.

If you try to detect buffer overflows using static analysis of the linux kernel what you need to do is to is go through the source code and define invariants. Those invariants are TYPES in languages powerful enough to express them.

For example the invariant that memory, or any resource allocated must be freed can be expressed in Haskell.

In C++ it cannot be expressed. There are workarounds like RAII, but that does not give any guarantees.

If you do not think type systems and thus languages make any differences, you also cannot believe that formal verification makes any difference, because type systems are a weak form of formal verification. How "weak" depends on the language.

You should also read up on the Curry-Howard correspondence to learn something about the deep connections between types, programs, and proofs.

http://en.wikipedia.org/wiki/Curry-Howard_correspondence

JavaScript would be terrible, because it's easy to hide unwanted behaviour in counter-intuitive corners of the language.

Besides the language peculiarities, a garbage collected or interpreted language is very vulnerable to side channel attacks because of the large amount of complicated behaviour that is being glossed over by the language runtime. (One example would be garbage collection rounds and timing attacks, but I'm sure smarter people would find tons of features that leak secret information. Another example is on-demand JIT'ing when code becomes hot in certain runtimes. The timing of such a JIT stall could publish information you thought secure.)