Applications of Barendregt–Geuvers–Klop conjecture
I'm not (exactly) an expert, but my understanding is that there are very few practical applications of this conjecture, except possibly simplifying the decision procedure for type-checking in normalizing theories, by allowing one to choose any reduction strategy with confidence.

My feeling about this conjecture is that it is an important litmus test on our understanding of normalization proofs in general, which at the moment (though this is rapidly changing) are somewhat ad hoc.

In particular, weak normalization proofs seem remarkably simpler, possibly due to weakly normalizing terms having the structure of a Partial Combinatory Algebra, which is not the case for strongly normalizing terms, as explained at length in a '93 paper by Hyland and Ong. Even simpler are proofs of existence of normal forms, which are the result of applying the technique of Normalization by Evaluation, which, IMO, are the "conceptually correct" proofs.

Given the difference of these 3 notions (SN, WN, existence of normal forms), one might be surprised that we have no examples of "natural" type systems where they don't all coincide (though for the latter 2, one can simply reason about the combinatorics of reductions). In the limited case of PTSes, this is what the BGK conjecture asks.

A satisfying resolution to the question would explain why a proof of WN or NbE can be promoted to a proof of SN, possibly by building a notion of normalization model which coincides in the case of PTSes. This desire for understanding is the principal motivation for the conjecture.