In this short paper, we advocate for the idea that continuation-based intermediate languages correspond to intermediate logics. The goal of intermediate languages is to serve as a basis for compiler intermediate representations, allowing to represent expressive program transformations for optimisation and compilation while preserving the properties that make programs compilable efficiently in the first place, such as the ``stackability'' of continuations. Intermediate logics are logic between intuitionistic and classical logic in terms of provability. The S4 modal logic can be seen as an intermediate logic owing to the Gödel-McKinsey-Tarski theorem, which states the intuitionistic nature of its modal fragment. In this paper, we propose a polarised sequent calculus for (classical) S4 modal logic together with an operational machine model with which we study the stackability properties of its modal fragment.