In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are `realized` by objects, known as `realizers`, in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many var...