This is my very superficial take from Thomas's brief presentation that gave a taste of an on-going project of his (with collaborators). The work refers to some objects of classic Mathematics; the definition of these objects transcends my understanding, but I found the proof strategy extremely fascinating.
For illustration, consider the following toy problem. We are given two algorithms, $A$ and $B$, and the guarantee that $A$ (resp., $B$) defines a monotonically non-decreasing (resp., non-increasing) sequence that converges to $a$ (resp., $b$); that is, $A(1) \leq A(2) \leq A(3) \cdots$ and $a=\lim_{i\rightarrow\infty} A(i)$ (resp., $B(1) \geq B(2) \geq B(3) \cdots$ and $a=\lim_{i\rightarrow\infty} B(i)$). Being guaranteed that $a$ is not bigger than $b$, we wish to prove that $a$ is strictly smaller than $b$. The proposed strategy is proving that either $a$ or $b$ cannot be approximated by an algorithm; that is, there exists no algorithm that given a positive $\epsilon$ outputs a number in $[a\pm\epsilon]$. The observation is that the foregoing is possible only if $a$ is strictly smaller than $b$, because if $a=b$ then we could approximate $a$ by finding $i$ such that $A(i) \geq B(i)-2\epsilon$ (and outputting $(B(i)-A(i))/2$). Note that, by convergence, there exists $i$ such that $A(i)\geq a -\epsilon$ (resp., $B(i)\leq b+\epsilon = a +\epsilon$).
The actual application of Thomas refers to proving that two infinite sets, $S$ and $T$, are different (or rather that $S$ is strictly contained in $T$). In his context, one define a class of functions $F$ over certain subsets of a universe that contains $T$ as well as a sequence of subsets $S_1,S_2,....$ of $S$ and a sequence of supersets $T_1,T_2,....$ of $T$ such that $S=T$ if and only if each function $f\in F$ it holds that $\lim_{i\rightarrow\infty} f(S_i)$ equal $\lim_{i\rightarrow\infty} f(T_i)$. Furthermore, there is an algorithm $A'$ (resp., $B'$) that, given a function $f$ and an index $i$, returns $f(S_i)$ (resp., $f(T_i)$. In contrast, it will be proved that the value of $f(S)$ cannot be approximated, which implies $S\neq T$. (That is, for a fixed $f$, we let $A(i)=A'(f,i)$ (resp., $B(i)=B'(f,i)$).)