I think usability is hard to judge because there isn't yet good tool
support to experiment with. But I believe that it can grow on the
user. A lock simply means "we've moved into a modal subterm". The
position of the lock in the context is important in order to keep
track of which variables were introduced before/after moving into
that modal subterm. When using a variable, you just need to make
sure that the variable's modal annotation is ≤ the composition of
the locks, i.e. the modality of the position where we currently are
and where we want to use the variable.
This is a reasonable point.
I
do think, however, that tool support is not necessary to evaluate
usability. A really usable theory should also be usable informally, as
in the HoTT Book and my BFP paper. This is what I have trouble with for locking modal type theories;
but it's certainly possible that I could train myself to do it. It certainly takes some mental training to use split-context modal type theories informally too.
A more serious and mathematical issue is that MTT requires all modalities to be right adjoints, semantically, because you have to have some operation to interpret the locking functors on contexts. (And FitchTT even requires those left adjoints to themselves be (parametric) right adjoints.) This seems a serious restriction on the kinds of situations we can model.
One can argue that the process of interpreting a split-context
theory involves building a new category of contexts (some generalized
kind of comma category, perhaps) that *does* interpret such context
operations, and therefore could also interpret MTT. But we don't have a
general theory of this yet.
To be precise, given an arbitrary 2-category M of modes, I would like there to be a corresponding instance of a general modal type theory that can be interpreted in any M-shaped diagram of suitable categories, with all the morphisms of M corresponding to syntactic modalities, and not requiring the existence of any additional adjoints in the semantics. The LSR fibrational framework achieves this for simple type theories, but I don't think there is any published framework that achieves it for dependent type theories.
Best,
Mike