website/about_me.md

title	displaytitle	showtitle
About me	$ whoami	true

I'm Tito, alias "tauroh". I'm a high school student living in Pavia, Italy. I was born in 2004. I have many more interests than I'm able to pursue and I still have to decide what to do after high school. Unless I undergo a sudden change in personality and hobbies, it will be something science-related. I'm quite a geek; I'm into maths and pretty much everything that has to do with computers. I used to play the piano regularly until last year but I don't have enough free time to study music seriously right now.

Maths

I have been fascinated by maths since I was a child, and my parents taught me where the elegance that some people (like them, and like me) see in mathematics really resides. Abstraction and formal logic are in my opinion the most advanced capabilities of the human mind -- the latest that evolution gave us from a biological perspective. 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 the most abstract and foundational aspects, often related to logic and philosophy: category theory, abstract algebra, type theory, model structures... Problem is, you're supposed to study a lot of undergraduate mathematics before proceeding with this areas. I haven't done that (yet); my mathematical background is fragile and therefore my knowledge is quite fragmented. I would like to study maths with a more consistent approach. Hopefully, that's what I will do after high school.

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).

I have taken part in the Italian Mathematical Olympiad with my school since my first year here. However, training and competitions are fun only with a team -- I perform much better in the team olympiad, and I don't really put the required effort and training in the individual competitions.

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

Computer science

Mathematics is hard: it's something I still haven't been able to get around. CS and programming are easier and that's why I spend a considerable amount of hours a day playing with my computer. Before examining my interests, 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 inherently 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'm currently studying the Haskell RTS and the STG machine (mostly during boring school classes). The GHC codebase is quite hard to read for a newcomer, and I'm still looking for a mentor! Sometimes I hang out on #haskell-it on libera.chat, the IRC channel of Haskell-ITA.

Hacking and cybersecurity

My low-level geek soul sometimes needs to take a break from lambda-calculi and theoretical CS and gets involved into hacking competitions called CTFs. I am part of Tower of Hanoi, the CTF and hacking 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 take part in the Italian Cybersecurity Olympiad, which targets high-school students. I got the second place at the finals in 2021.

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.

[comment]: # vim: ts=2:sts=2:sw=2:et:nojoinspaces:tw=80

---

1. Did you know that mathematical induction and recursive functions are basically the same thing? ↩︎

2. Such as the Curry-Howard-Lambek isomorphism! ↩︎