Realisability was originally designed by Kleene in order to build models of intuitionistic arithmetic (Heyting Arithmetic) as a kind of synthesis between Gödel's Dialectica interpretation and Brouwer-Heyting-Kolmogorov interpretation. Indeed the basic idea is to extend the notion of justifications of mathematical statements from (formal) proofs to programs thus defining the notion of a formula justified (proved) by a program.

Kleene used (indices of) recursive functions for his programs, but rapidly realisability was adapted to other formalisms, mostly based on lambda-calculus. Also realisability was soon seen to be also extendable to classical theories, but not as a primitive notion since one has to use a Gödel's like not-not-translations to transfer the semantics from intuitionnistic to classical logic.

It is thus not a small achievement that Krivine at the end of the nineties could define a direct notion of realisability for classical logic. In a first step the semantics was defined for higher order arithmetic, then further extended to full set theory by finding realisers for each axioms of ZF. Interestingly enough these realisers are all very simple programs, but the one for the extensionality axiom which implements a real algorithm (essentialy a while loop).

The so-called classical realisability thus allows to define new semantics for arithmetic, analysis and now set theory in which the truth value of a formula is the set of its realisers. Krivine has shown that this construction can be seen as an extension of Cohen's forcing, but with some very new properties (eg, contrarily to forcing, ordinals are not preserved between the base model and the realisability model) that are almost all yet to be discovered and understood...