I think the formalist dream (Hilbert's programme) has turned out not to work. Sure, For All Practical Purposes (FAPP), it is still a useful tool, but it has its limits (Goedel).
And in fact that shouldn't surprise us. After all, formal logic is nothing else but a game of finite sequences of a finite set of symbols that satisfy certain formal rules. Formal logic is the study of a certain set of mappings which map {1,2,...n} into, say, the ASCII set. It only has a meaning when we GIVE it a meaning - and that's Platonism, no ?
I'd even say, for this formal game to have a meaning in the first place, you'd already have to ASSUME certain properties of natural numbers, in order to be able to say things about these mappings from {1...n} into the ASCII set. So using then this formal game to PROVE properties of natural numbers seems to be a bit circular IMHO, because you've USED certain properties of the natural numbers to set up the formal machinery in the first place.
For instance, how do you prove that every natural number has a successor, purely formally ?