Super exciting new results on this CSL paper Frank and I are trying to work on.
What's interesting to me is that in typical logics, unlike typical programming languages, there are good metrics of what it means to have an embedding that isn't trivial. Like if you get a good flamewar going between an ML hacker and a LISP hacker, the ML will point to their ability to make a type of sexps and shove all of LISP in there, and the LISP hacker will think that an ML typechecker is only willing to compile a fraction of the sensible programs in the world, and only in a funny irregular syntax at that.
But! It is possible to embed focused classical logic into focused intuitionistic logic (and not the opposite) in a sensible primitive-recursive sort of way that preserves focusing --- I hear via Frank that he just worked this out in a conversation with Evan and Kaustuv not so long ago. To preserve focusing is a really strong condition.
And I think we've worked out further how to embed just about every substructural logic I've ever heard of to this same high degree of faithfulness into just the negative connectives of focused first-order linear logic. And it yields cut-elimination, identity, a focusing system, ad completeness of focusing for all those logics for free.
Of course, something could have gone wrong, but that's always the case until you've finished writing it up...