The translation you are referring to is the Gödel-McKinsey-Tarski translation. Actually, the S4 translation of intuitionistic P → Q is □(□P → □Q) which can be understood informally as: I can prove that a proof of P can be converted into a proof of Q. Intuitionistic ¬P translates into classical S4 as □¬□P which can be understood as: I can prove that there is not a proof of P.
A constructivist can undertand classical S4 □P as saying that P is provable. But there is no simple constructive way to understand classical ◇P. Classical ◇P says in effect that it is not the case that not-P is provable, but without constructing a proof to show that this is so.
This is analogous to how classical (∃x)Fx says that something is F, but without constructing it. However, we can use the double negation translation to represent classical (∃x)Fx within intuitionistic logic as ¬¬(∃x)Fx. If we use intuitionistic modal logic, then we might be able to represent classical ◇P as intuitionistic ¬¬◇P. In practice, the interpretation of ◇P in intuitionism depends on context, so I am not confident this would always work.