Computability-theoretic results relevant to realizability This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of computability theory itself don't seem too relevant for realizability as far as I can tell. For example, I don't know of any result in realizability which relies on (say) the Low Basis Theorem or on the solution to Post's problem. Basic computability of course plays a role - e.g. whipping up realizability semantics appropriate for computability notions which lack universal machines, such as the primitive recursive functions, is difficult and interesting - but (to my practically-nonexistent knowledge) the deeper results don't seem to play a role.
My question is whether this is accurate. In particular, I'd be extremely interested in any significant role played by priority arguments in realizability.
The most relevant thing I've found is Charles McCarty's paper "Realizability and recursive set theory", which established a connection between isols/recursive equivalence types and realizability. There are many results about isols, of course, which are proved via complicated priority arguments. However, unless I'm missing something this seems to be a situation where realizability sheds light on the isols, rather than results about isols being relevant to realizability.
 A: Many results of computability theory can be stated synthetically in the effective topos. I have dubbed this idea "synthetic computability" and have tried to develop as much computability this way as I can. Some examples of how classical theorems in computability theory are stated synthetically:

*

*"There is no computable enumeration of total recursive functions" becomes "The set of functions $\mathbb{N} \to \mathbb{N}$ is uncountable" in the internal language of the effective topos.

*"There is a computable enumertion of computably enumerable sets" becomes "There are countably many countable subsets of $\mathbb{N}$".

*"There is a c.e. set whose complement is not c.e." becomes "there is a countable subset of $\mathbb{N}$ whose complement is not countable".

*"There is an immune set" becomes "there is a subset of $\mathbb{N}$ which is neither finite nor infinite".

One can keep going this way. So far I have been stuck on obtaining a suitable synthetic definition of Turing reducibility. I have one, but I am not completely happy with it. Intermediate degrees are also out of my reach, although it looks like they should translate to results about measure theory, or perhaps descriptive set theory, I am not sure. Essentially, a priority argument feels a bit like showing that a certain intersection of open sets is non-empty, but it's subtle.
The only other place where I would look for the kinds of results that you are asking about is perhaps the work of Jaap van Oosten, in particular his study of the subtoposes of the effective topos (I am not sure how much is published). It seems exceedingly hard to get a grip on the Lawvere-Tierney $j$-operators in the effective topos, and this may be related to some complicated structures in computability.
There is a general principle: in order for a result $A$ in computability theory to have significance in realizability, you need to find an intuitionistic statement $B$ such that validity of its realizability interpretation is related to $A$. I started to study synthetic computability more seriously when I discovered that the Recursion theorem corresponds to a variant of Lawvere's fixed-point theorem (see this paper1).
Until we find out what priority arguments correspond to under realizability interpretation, we pretty much have no clue how to use them.
1Bauer, Andrej, On fixed-point theorems in synthetic computability, Tbil. Math. J. 10, No. 3, 167-181 (2017). Author's website, ZBL1403.03076, MR3725758.
