Why Constructive Modal Logics?

I guess the question can be taken as both why constructive?, if we like modal logics, but also as why modal?, if we favor constructive logic. (some might even ask why logic at all?, but we won't go there...)

I will try to outline my answers to both forms of the question.

To my functional programming friends, the answer to why modal? goes via extending the  Curry-Howard paradigm to deal with effects, exceptions, I/O and other non-pure features of real-life computations. Despite all the excellent work in this area in the last thirty years or so, the models and tools we have still seem to work best for sequential, effect-free functional programming. The hope is that extending the Curry-Howard to more modal systems will allow us to deal with more of the computing we already do, but are not able to model accurately.

To my modal logicians friends, the answer to why constructive? goes via pointing out the affordances of Curry-Howard as well as the niceties of having an amenable proof-theory with explicit computational content.

 I still believe what we wrote in the preface of the special issue devoted to IMLA in 2004, viz.   `Proofs carry concrete intensional information over and above the fact that a formula is valid. From this point of view modalities come in naturally, viz.\ as syntactic reflections of this underlying intensional level hidden in the proof theory of a constructive logic. A constructive modal logic might arise in an attempt to handle the intensional dimension, or parameter, of modalities (time, nondeterminism, security margin, knowledge, beliefs, etc.) in a computational way at the level of the proof theory. It seems obvious that such a program has much to offer not only from a computer science perspective.'

However I will freely admit that putting together constructivity and intensionality in the guise of constructive modal logics is not an easy task, as there are many design decisions to take and these do not seem clear cut to me. Even the definitions of systems are up for grabs, so there is very little known about semantics and/or complexity results, for instance. Worse still I cannot point out at huge successes in the form of logically-based systems being used in real applications. The best I seem to be able to do is point out at (many though!) systems that use ideas from the Curry-Howard correspondence...