Applications
Realizability is one of the methods used in proof mining to extract concrete "programs" from seemingly nonconstructive mathematical proof. Program extraction using realizability is implemented in some proof assistants such as Coq.
Read more about this topic: Realizability