How I became a logician

I personally don’t like to call myself a “logician” but I guess it describes pretty well what I was. During my doctoral thesis, I couldn’t call myself a mathematician (I’ve never had a course on algebra), I couldn’t call myself a computer scientist (I actually started my studies with computer science but I’ve drifted farther and farther from it with time) and finally, I couldn’t call myself a philosopher (I don’t have any education or culture in philosophy). In this blog post, I would like to tell how I ended up in this identity crisis by naively pursuing simple obsessions.

A simple kid

I was a very average student. I didn’t really understand how to study. I had no interest in school and I found school quite difficult. I was more interested in playing, creating and experimenting. My first experience with programming was when I decided to learn programming in Ruby in order to create scripts for RPG Maker XP (a software made to create role-playing games). Then, I learned the C++ language. Honestly, I wasn’t especially good at it and I wouldn’t say I was particularly passionate about programming itself but I enjoyed the feel of it very much.

At the end of high school, I had to think of my future and programming was the only thing I could do that I saw a future in. So it was quite natural that I chose to go towards computer science. Even though I wasn’t very smart, I was rather obsessive about things. I was quite obsessed with understanding the mind. I was already interested in psychology and psychiatry. Out of the blue, I decided that I wanted to learn about computational neuroscience. Why? Because it sounded cool but I had strictly no idea what it was about. And my first reflex was to ask random people on the internet.

Discovery

I quickly understood that it wasn’t really for me and actually after learning what it was, I wasn’t really interested anymore. But during the process, I came across weird keywords like “graph theory”, “artificial intelligence”, “lambda-calculus” or “Turing machine”. I was innocent so I just asked for references and explanations in the “Programming” section of a famous French forum about video games (yeah). I then received a private message from “Jérémy”, a student of a school I had never heard of: Ecole Normale Supérieure (ENS). From that started months of exchanges starting from the summer after the end of high school…

Jérémy told me about a world I never thought existed: research in computer science (the concept of a programmer in a lab coat was so weird to me). I asked so many questions about everything. He told me about the Curry-Howard correspondence: the fact that some computer programs correspond to mathematical proofs and vice-versa. I ended up asking questions about type theory, formal proofs, sequent calculus, lambda-calculus, natural deduction, functional programming and even did exercises with him. I was sometimes going to the library (something which I never did before) to read books about logic and theoretical computer science, and I was just attracted to the aesthetics of it. The lines. The symbols. The graphs. The geometry. Logic (mind, reason, abstract, mystical) was concretely connected to the down-to-earth computation powered by electricity and powering video games. It felt like discovering something very fundamental. A secret yet to explore: the mystery, the simplicity and the authority of saying “it’s logical”.

The teachers I had in university were the first researchers in computer science I had met and I always flooded them with questions about their job and ended up catching the attention of a researcher who challenged me with exercises on Turing machines. At the end of my second year I had to do an internship. I remember creating a post on “Le site du zéro” (a French forum about programming) asking where I could find an internship related to my interests. I did not really realize how unusual it was but I actually did receive an answer from a PhD student at Inria Paris who suggested we meet. And that’s how I ended up with an internship on the formalization in Coq of the security guarantees in the compilation of an imperative language.

Digging until bedrock

Since I had excellent results in my 2-year technical degree, I was expected to go to an excellent engineering school but I chose to go to the third year of “licence informatique” in the Paris Diderot University which was holding one of the most important research teams on the Curry-Howard correspondence. There was also an elite master’s degree called “MPRI” and Jérémy told me that I had to go there to follow my interests.

During our exchanges, Jérémy often joked about a man called Jean-Yves Girard. He told me that his Blind Spot “course on logic” wasn’t a standard course on logic and that he couldn’t recommend it to me. That’s precisely why I searched for it in libraries and started to read it. And that’s how I ended up in an unpaid research internship on the simulation of the PCF language into the proof-nets of linear logic (I didn’t really understand what it was about but I explicitly wanted to work on linear logic).

From there, it was mostly about climbing the ladder to understand what was at the end of all of that and find what was the most advanced understanding of the relation between logic and computation. And I believed that Girard had it and that I just had to understand everything from him step by step. That’s how I started a research work on Girard’s geometry of interaction in my first year of master and on Girard’s transcendental syntax in my second year (at MPRI, that Jérémy recommended to me). Then, Thomas Seiller gave me the opportunity to start an unusual PhD thesis on Girard’s transcendental syntax: a demanding work with very few references but an ambitious project touching everything in logic and computer science, questioning what logic is truly about.

It’s not the end

Without noticing, I entered a world in which I didn’t fit by pursuing something greater than me, which seemed to explain simple things that were literally omnipresent and ordinary in our existence. But what I describe as a spiritual experience may be mere voyeurism. I wanted to see logic naked. And I believe I could see it. But it became part of a big and out-of-reach landscape.

Now, I’m no longer in academia. There’s no next step I can just follow and that already exists somewhere. Actually, I didn’t think being in academia would allow me to see what I wanted. I had to see something else, something different. But that probably doesn’t make me a logician anymore.

Nonetheless, the wish to unfold the nature of logic and computation hasn’t faded. But the path is completely fogged. What to look for? What to look at? What more is there to say? What more is there to see? How can I see more? One thing I’m sure of: it won’t be the work of a single man.