 Finally it should be noted that CH formalism, if we can call it such, will be unacceptable to the formalist who is motivated by anti-platonist concerns and wishes to exclude abstract objects from all mathematics, including metamathematics. For the meanings of concrete utterances of mathematical formulae, according to CH formalism, are sets/species/types of proofs, and the latter are abstract objects, infinitely many of them, of arbitrarily long finite length. The problem of the metatheory, in other words, has not been met. The anti-platonist cannot straightforwardly lift the ideas of syntactico-semantics and apply the CH correspondence in support of anti-platonism; a great deal more philosophical work is required.