In mathematics and the theory of computation, what is interesting is what is incredible but true, defying our intuitions, giving new light to our understanding. This is of course the case for all sciences, and even (more?) for engineering, with "true" replaced by "doable".
In the theory of higher-type computation, in the sense of Kleene and Kreisel, my favourite example is the characterization of the sets that can be exhaustively searched by an algorithm, in the sense of Turing, in finite time, as those which are topologically compact.
In particular, this understanding gives examples of infinite sets that can be completely inspected in finite time in an algorithmic way, which perhaps defies intuition.
I am also interested in constructive mathematics, which I see as a generalization, rather than as a restriction, of classical mathematics. In constructive mathematics, in the way I conceive it, computability is a side-effect, rather than its foundation.
What distinguishes classical and constructive mathematics is that the latter is better equipped to explicitly indicate the amount of information given by its definitions, theorems and proofs. This is particularly the case for Martin-Loef type theory, and even more for its univalent extensions.
The above is a (probably misleading) hint of what my research is about.
directions: Look for building Y9 in the yellow zone of the Edgbaston campus map. This is about 1 minute walking time from the train station. Turn left when you exit the station, and walk for about 30 meters. Our building is the right-hand one of two red-brick twin buildings facing each other.