 On the first point the formalist will, of course, be a formalist! She will link correctness, at least at the most fundamental level, to formal proof. Here, then, the CH correspondence, or better correspondences, are surely very attractive to the formalist. The linkage between propositions and computations, algorithmic reductions of terms coding proofs to irreducible normal forms in particular, fits very snugly with those versions of formalism which take mathematics to be, at heart, shuffling of symbols with no external reference.