$ whoami

I’m Tito, alias “tauroh”. I’m studying for a bachelor’s degree in Maths at the University of Pavia, in Italy. I’m into maths and pretty much everything that has to do with computers, except front-end development.

Maths

When you get to really appreciate maths, you discover a brand new world. Unfortunately, that’s something that school is not able to teach – that’s why many people still think that maths is made of formulas, exercises and grades.

As you might have understood, I like pure mathematics, and specifically its most abstract and foundational aspects, often related to logic and philosophy: category theory, abstract algebra, type theory, model structures…

I spent some time studying Categorical Quantum Mechanics, a mathematical setting for quantum physics in dagger-compact categories (such as the one of finite-dimensional Hilbert spaces and linear maps) originally introduced by Abramsky and Coecke. It has some interesting foundational implications on operational postulates and diagrammatics for physics. I also wanted to know whether I had really understood how does a proof checker work – so I put the two things together! I wrote a partial formalization of these categorical structures in Coq. The sources can be found on my GitHub (it uses @jwiegley’s category theory library).

While attending high school, I took part in the Italian Mathematical Olympiad. This exciting experience led me to study maths.

The nLab is a nice play to get lost in during cold winter nights with a cup of tea.

Computer science

I have to stress that I really happen to hate frontend development and weakly typed programming languages. This website doesn’t depend on 50KB-sized DOM-diffing JavaScript frameworks and it never will.

My approach to computer science is dual. Just like in mathematics, I like abstract and theoretical areas of CS: functional programming, dependently-typed¹ proof assistants, type theory (again!)… On the other hand, I want to understand how things work at the lowest level and I’m often busy reversing some crappy x86 ASM code or studying network security and operating systems internals.

Functional programming and theoretical CS

Haskell is an awesome language and GHC is an astonishingly well-engineered piece of software. Functional programming in general has some interesting properties related to pure mathematics and logics². Apart from theoretical and academic topics, I’m interested in the implementation of call-by-need referentially transparent functional languages and I’ve spent some months studying the Haskell RTS and the STG machine (mostly during boring high school classes).

Hacking and cybersecurity

I like playing hacking competitions called CTFs. I am part of Tower of Hanoi, the CTF team from Politecnico di Milano (although I’m not a student there). Staying up all night looking at disassemblies and memory dumps has some kind of inherently mystical meaning, and it’s also good fun.

People from ToH were the first to introduce me to offensive cybersecurity during the CyberChallenge.IT 2021 project. I also took part in the Italian Cybersecurity Olympiad, which targets high-school students. [I won the finals in 2022][olicyber-classifica22].

Apart from my technical interests, hacking history is an interesting topic on its own, and the underground scene that started to fade away a few years before I was born had a deep impact on technology as people use and know it today – and also on our economy and our society. If this is eye-catching to you, Bruce Sterling’s The Hacker Crackdown is a good read.