 On the second point, further work on the CH correspondences generalised the results from intuitionistic logic to a wide variety of other logics, in particular to classical logic (Griffin, 1990), as well as to other logical frameworks such as modal logic and linear logic. There is no burdensome logical restriction imposed by ‘Formulae-as-Types’ then, no need for the formalist to fight with one hand tied behind her back.