sentences:  The realizer, however, usually gives more information about the formula than a formal proof would directly provide.Beyond giving insight into intuitionistic provability, realizability can be applied to prove the disjunction and existence properties for intuitionistic theories and to extract programs from proofs, as in proof mining.It is also related to topos theory via the realizability topos.