What logic correponds via Curry-Howard to a Monad? 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?
The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and then translates Moggi's metalanguage into it.

Both papers note that the axioms of a strong monad were originally introduced by Curry in 1952, which was independently re-invented by Fairtlough and Mendler as lax logic. Giving the action on types and contexts below, we see:

$$
\begin{array}{lcl}
( \to )^+ &amp; =&amp; ◻^+ \to ^+ \\
(◯)^+ &amp; = &amp; ◊◻^+ \\
^+ &amp; =&amp;  \;\;\mbox{for atomic}\;  \
\end{array}
$$

The translation of Davies and Pfenning is very similar to Gödel's embedding of intuitionistic logic into classical logic, and to Girard's embedding of intuitionistic logic into linear logic.