* So the endofunctoriality of modalities is totally standard (to put it another way, it's obvious that their kind is type -> type) but after seeing so many instances of Gamma |- M : A@w in tom's presentation, I start to wonder if all the "@w"s are just funny backwards notation for what is morally an endofunctor application. That is, are modal worlds themselves just a funny sort of type operator?
Wait, no, now that I think about it, you don't get <>A -> <>B from A -> B, so maybe they're not really functors, just type operators. Then again, (A -> B)@w is the same as A@w -> B@w, so maybe that works still.
* This is sort of suggested by ultrafinitism: what sort of axiomitzation would correspond to posssible-world models with an accessibility function (taking values in some ring, somehow compatible via a triangle-like inequality with transitivity of accessibility) in place of an accessibility relation? The analogy to ultrafinitism is "I believe in proofs at most k symbols long" compared to "My imagination is powerful enough to imagine a possible world k different than my current world", or, in tom's case, putting some sort of resource bound on how much time mobile code could take, i.e. "this host is distance/latency k from this other host on the network".
* Found a link crediting a guy named Lewis for inventing the concept of modal logic in 1918. I'm bothered that I've never heard of him before. Always thought Kripke was the one big name.