But... viewed semantically, I like that focusing appears to simplify an existing mess, (or at least all of the mess is carefully tucked away in the shift operators) in contrast to the proof-theoretic case, where it makes the proof system a bit more messy (but in a way that has obvious benefits). If Andreoli hadn't figured it out from the angle of optimizing proof search, I feel like you'd still want to have invented focusing just to clean up the phase semantics.
Of course the really weird thing to me is that by doing semantics at all, I'm working in the ambiently classical world of set theory --- and basically the identical set of "semantic" clauses give the same result of capturing ILL when I interpret them proof theoretically, i.e. in an ambiently intuitionistic world. My best guess is that the foralls in the definition of the shifts are hiding what's effectively a forall over kripke worlds.