The reservations seem rather unqualified indeed. A lot of strawman argumentation to begin with (singling out specific subjects of CS the authors deems unworthy). But even about PCC I don't think the author has the right notion. It is not the same as type checking. As an example, at my old university department they created a proof of the euclidian algorithm and extracted a program from it that would compute the gcd. That way you have more than a syntactically correct program, you have a proof that the code actually gives you the gcd. And yes, it was very academic, but still.
Also, if CS is so useless, how come most leaders in the Netflix challenge seem to be CS departments?
Also, when you're examining something that dubs itself "science," pointing out a spot of routine dishonesty, however small and irrelevant, is hardly indicating a "strawman." Shades of the [Curate's egg](http://en.wikipedia.org/wiki/Curate's_egg). I'm sure most of the entries on Enron's balance sheet were perfectly accurate, as well.
Yes, but how does one area of research of CS being pointless spoil the other areas? I don't think it is a curate's egg at all. I don't want to claim that CS is not spoiled, though. The patronage thing might be a problem. However, research topics do have to compete even in science - they may not be exposed to judgement by the general public, as are companies, but internally, there are mechanisms of selection. Probably not the best ones, but still. And if too much money would flow into obviously useless research, there might even be a public outcry.
It spoils the others because the relationship between science and personal honesty is extremely close and important. Science has to be utterly intolerant of nonsense. Its spirit is to attack it and take no prisoners. If you have this spirit - like D.J. Bernstein - you will not be welcome in any CS faculty that exhibits curate's egg nature, for fairly obvious reasons.
(I'm a particularly big fan of DJB because his very existence is a sort of counterattack - he's a programmer who's infiltrated the math department! Unfortunately there is only one of him, but we could certainly use a dozen more.)
I think what you are describing is program verification, not proof-carrying code.
In proof-carrying code, of course, the proposition you are proving may not be associated with the source code as an invariant. But if it isn't, why isn't it? It makes no sense to have one language for the invariant and another for the program.
For example, one use of PCC is to prove propositions about a bit of machine code, such as a packet filter. When you create an environment that can state propositions about machine code, you have created a typed assembler, whether you like it or not.
Most leaders in the Netflix challenge are (at) CS departments because CS departments are full of smart programmers.
Also, if CS is so useless, how come most leaders in the Netflix challenge seem to be CS departments?