What a great presentation!:-)

Think I will tackle rz next.

(re Single Value Theorem, "except" not "expect")

This may be a very silly question, but has the approach via synthetic computability ever led to the discovery of any new results in computability theory/recursion theory (rather than simply the organization and clarification of old knowledge)?

Either way, I think it's a great idea (even The Right Idea), in much the same fashion as, say, I would now consider the approach to forcing arguments via topos theory/sheaf theory to be, in some sense, The Right Way. However, in that case, to the best of my (admittedly limited) knowledge, no previously unknown results in set theory were ever discovered via the categorical methods; merely a deeper understanding and organization of old ideas achieved. I am curious if the situation with synthetic computability is similar. [There may be some confusion in even trying to compare these; I suppose synthetic computability theory doesn't itself deal with the construction of the models in which it is to be interpreted (are there interesting models other than the effective topos?), but rather simply amounts to providing the appropriate axioms, language, and styles of reasoning with which to carry out arguments within those models]

Again, apologies if the question seems misguided in some way or if I've made any mistakes of understanding.

Your questions are right on the spot, actually. They apply quite generally to any reformulation of an old subject. It would be interesting to look at examples from history.

You asked whether there are any new results in computability using synthetic computability. First I should remark that in principle any such new results can always be proved using "standard" methods. This of course is quite beside the point. I am aware of three new results, but two of those are not published yet. First, I have an unpublished covering theorem for computable complete separable metric spaces (CSM) which I discovered synthetically. It states that if a countable family of closed balls of a CSM cover the space, then their interiors already cover the space. An immediate consequence of this is the BD-N principle and the KLS theorem (in general form, for all CSMs). Second, my student Davorin Lešnik and I have a synthetic proof which generalizes a result of Friedberg's, who showed that the intrinsic topology of Baire space is finer than the metric topology. We showed this already happens for other, much simpler spaces, such as the one-point compactification of the natural numbers. This is also unpublished, but is soon going to be submitted for publication. The third, published result is the one on Banach-Mazur computability, published in a joint paper with Alex simpson. That one is not strictly "synthetic" but we certainly would never would have discovered it without first doing the "synthetic" (constructive) embedding theorems.

You also ask if there are other models apart from the effective topos. Yes, for example an "effective" topos built from oracle machines. In other words, synthetic computability relativizes throughout so that anything proved synthetically automatically holds relative to an oracle. Are there other, wildly different models? I do not know. I would expect there to be variants of realizability that validate only parts of synthetic computability.

Very nice presentation! I am not familiar with this area, so I have a very naive question. Have people looked at resource-bounded topoi, to study computational complexity questions? Are there some obvious reasons why something like that would be hard to achieve?

@Manoj: You cannot just dream up a topos. I never heard of a "resource-bounded" topos, and I think there is no such thing. Intutionistic logic is not resource-aware and you have to pass to some sort of restricted logic, such as Sam Buss's systems.