> Those who verify software have access to the source, open or not.

That's not true. Black hats are essentially verifiers, and they generally do not have access to closed source.

How do you look at the last 15 years worth of Microsoft Windows OS advisories and conclude that closed source has prevented hats of all colors from discovering vulnerabilities?

Why do you keep raising this straw man? It is obviously possible to reverse engineer object code and find vulnerabilities. But it is (equally obviously) easier to examine source code to find vulnerabilities.

This slippery slope goes in both directions. Software is also easier to audit when it's built in higher-level languages, but we don't have ideological objections about verifiability to software written in C.

I'm not sure I understand what you mean by that. Do you mean that people think that it doesn't matter what language code is written in as long as it is open source? I certainly don't believe that. It's pretty clear to me that C is a terrible language for writing secure code. (But coming up with something that is actually better than C is not so easy.)

All agree that higher level (e.g. C) is easier to reason about than lower level (assembly).

Now, you say that open source (e.g. C) is not only easier, but qualitatively different: open source good, closed source bad.

tptacek points out: higher level (e.g. Haskell) is easier to reason about than lower level (e.g. C) - maybe even qualitatively.

So, why are people only complaining about closed source, when they should (by analogous reasoning) be complaining about code written in C? Granted, it's possible to analyse, but it's obviously easier when it's written in Haskell!

For what it's worth, I complain about code written in C too.

Here might be something to look for among those advisories: how many of them were discovered in the source versus in the field.

If the vendor is lazy about verifying code, it being closed is a big disadvantage. "We're not combing the code for bugs, and neither is anyone else; if it's not reported to us, it doesn't exist."

They are verifiers who cannot, with straight faces, declare a body of code verified.

I'll bet some of them can.