Something that I think I knew but that I hadn't ever fully internalized is the degree to which the developments and checks recommended by the judgmental methodology are much closer to what you want when defining a programming language (where type safety - progress and preservation - are primary concerns) than what you want when defining a logic (where consistency, which is a sort of normalization property, is a big concern).
A really, really high level picture of the methodology followed by Pfenning and Davies is this:
- Define a substitution principle
- Show that everything that looks it should be a reducible expression (redex) is actually, you know, reducible (local soundness)
- Show that everything that has an interesting type can be η-expanded (local completeness)
- Check that the substitution principle which you claimed to be true and possibly used in the previous two steps actually holds
Is it really the case that the only "more interesting" part of type safety theorems is the fact that programming languages have values - places where, in practice, you want to stop with all of this reducing business - and the safety proof has to show that these uses of values are somehow consistent with the desired progress theorem? And has the "progress-ey" part of local soundness been considered elsewhere? Certainly the preservation-ey part is well-known enough to have its own name, "subject reduction." It seems like the kind of discussion that would be natural to find in the hybrid child of Proofs and Types and TAPL, but I don't believe such a book exists.