When you say "standard semantics" for higher order logic, this takes you well out of the realm of proof systems. It is true that the set of validities in first-order logic is recursively enumerable, so we have a hope of coming up with a recursive proof system which can prove all validities (and in fact plenty of such systems exist); however, for higher-order logics this is wildly false. These computability theoretic considerations rule out any hope of any kind of proof system for higher-order logic.
That is, your first two paragraphs are conflating some things:
It is true that the set of true sentences of higher-order logic is not recursively enumerable. But this is already true of first-order logic.
Fixing a given proof system, of course the things it proves are recursively enumerable.
But you're really interested in the sentences which "ought to be provable," that is the validities. In the context of the standard semantics, the set of validities is incredibly complicated ($\Pi^1_1$-complete, almost unimaginably more complicated than recursively enumerable); in the context of the Henkin semantics (http://en.wikipedia.org/wiki/Second-order_logic#Semantics), though, the validities are recursively enumerable.
Short version: for the standard semantics, no proof system can exist for purely computability-theoretic reasons. (There are also model-theoretic obstacles, such as the failure of compactness.)
But if you're interested in proof systems for higher-order logic, then you're probably interested in the Henkin, not standard, semantics. In this interpretation second-order logic is not really any different from first-order logic, and there do exist proof systems which will prove all validities. If your question is whether there are specific ones which are useable in practice, you have to be careful what you mean. Since the set of validities is incomputable, we can't hope for an algorithm which - on input some sentence $p$ - will answer "is $p$ a validity?" All we can hope for is a function enumerating the validities. But at this point it's not clear what "usable" means, so I don't have any answer.