A couple comments 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. We basically showed that graduality + extensionality determines almost all of the behavior of casts. 2. Exception handling for type errors is actually in direct conflict with graduality. The reason is that the type error is the least element and every term has to be monotone with respect to the type error, so if you catch a type error, to be monotone you have to show that the result you produce is less dynamic than the result you would have produced if there was no exception. This means that if you want to catch type errors you need to have a fancy catch form, or you need to do it at an "extra-linguistic" level, or you can use modal types (think monads) to say that catching a type error is a "reflective" operation and so any code that does it is uses the reflection modality.
Also as a side-note, in my opinion profunctors are an essential component of category theory, and it's really a shame that in intro courses we explain everything in terms of adjunctions, limits, presheaves, etc when profunctors are ultimately simpler. They are unavoidable when you do enriched/internal category theory and they are more directly useful in designing type theories than adjunctions.