I want to say something I found shocking and interesting.

Three weeks ago, a mathematician, Georg Lehner, approached me by email to say that he applied a result of a paper of mine to a paper of his.

The interesting thing is that in that paper of mine I redeveloped the patch topology both point free and constructively. (Although I was careful to say only in the last line of the introduction that, by the way, this paper is constructive, as a hidden message.)

But Georg managed to use this to make progress in classical mathematics, on Algebraic K-theory of stably compact spaces.

It is kind of shocking that a paper on constructive mathematics helps to make progress on classical mathematics.

But I rather like this, because, as I have said repeatedly here, I believe there is only one mathematics, of which classical and constructive are just two branches.

Moreover, I have witnessed the interaction of these two branches quite vividly in the last 25 years, in conferences I have attended, and in publications.

The interaction goes both ways.

And, by the way, Georg is here this week at 7WFTop in Venice, where he gave a talk about a different subject, namely measure theory via locales, which was both quite interesting and rather well delivered.

There is only one mathematics, of which both classical and constructive mathematics are branches, and, since at least the 1960's with the advent of topos theory, interact with each other.

The interaction is only getting more intensive and healthier.