According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural transformation $\eta: Id \to T$ and $\mu: T^2 \to T$ that arise out of an adjunction. Monadic Equational Logic limits one to a single formula on each side of the turnstile such as $x_1 : \tau_1 \vdash_{pl} e: \tau_2$.
In order to go beyond monadic equational logic to allow programs of the form $x_1: \tau_1, \dots, x_n:\tau_n \vdash e: \tau$ one needs an extra strength natural transformation
$t_{A,B}: A \times TB \to T(A \times B)$
This allows one to take a context $\Gamma$ into account, represented by the $A$ in $t_{A,B}$ above.
This corresponds to the formula in modal logic
$A \land \diamond B \supset \diamond(A \land B)$
which is logically quite weird as it would allow one to have propositions $A$= "S can board the plane" and $B$="S cannot board the plane" and reason "S can board the plane and it could have been the S cannot board the plane" to "it is possible that S can board the plane and that S cannot board the plane".
Moggi writes in his conclusion:
The semantics of computations corroborates the view that (constructive) proofs and programs are rather unrelated, although both of them can be understood in terms of functions. Indeed, monads (and comonads) used to model logical modalities, e.g. possibility and necessity in modal logic or why not and of course of linear logic, usually do not have a tensorial strength. In general, one should expect types suggested by logic to provide a more fine-grained type system without changing the nature of computations.
Have I understood this correctly? Is the Curry-Howard isomorphism for monads illogical?