Andrej Bauer has published a draft of his lectures on realizability: Bauer, [2022] “Notes on realizability”.
Realizability can be understood as a weaker/generalized version of the Curry-Howard correspondence, i.e. the idea that logical proofs can be interpreted as programs - in the case of realizability not necessarily total or even typed.