107 lines
5.0 KiB
Markdown
107 lines
5.0 KiB
Markdown
---
|
|
title: About me
|
|
displaytitle: '$ whoami'
|
|
showtitle: true
|
|
|
|
---
|
|
|
|
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][ct], [abstract algebra][abstract-algebra], [type
|
|
theory][type-theory], [model structures][simplicial-sets]...
|
|
|
|
I spent some time studying [Categorical Quantum Mechanics][cqm], 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][coq]. The sources can be found [on my GitHub][titos-catqm]
|
|
(it uses @jwiegley's [category theory library][coq-ct]).
|
|
|
|
While attending high school, I took part in the Italian [Mathematical Olympiad][olimate].
|
|
This exciting experience led me to study maths.
|
|
|
|
The [nLab][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[^rec] [proof assistants][agda], 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][hs] is an awesome language and [GHC][ghc] is an astonishingly
|
|
well-engineered piece of software. Functional programming in general has some
|
|
interesting properties related to pure mathematics and
|
|
logics[^curry-howard-lambek]. 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][ctf]. I
|
|
am part of [Tower of Hanoi][toh], 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][cyberchallenge] project. I also took part in the
|
|
Italian [Cybersecurity Olympiad][olicyber], 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][the-hacker-crackdown] is a good read.
|
|
|
|
[^rec]: Did you know that mathematical induction and recursive functions are
|
|
basically the same thing?
|
|
[^curry-howard-lambek]: Such as the [Curry-Howard-Lambek
|
|
isomorphism](https://wiki.haskell.org/Curry-Howard-Lambek_correspondence)!
|
|
|
|
[abstract-algebra]: <https://ncatlab.org/nlab/show/group>
|
|
[agda]: <https://wiki.portal.chalmers.se/agda/pmwiki.php>
|
|
[coq-ct]: <https://github.com/jwiegley/category-theory>
|
|
[coq]: <https://coq.inria.fr>
|
|
[cqm]: <https://arxiv.org/abs/1804.02265>
|
|
[ct]: <https://ncatlab.org/nlab/show/category+theory#abstract_nonsense> "i.e. abstract nonsense"
|
|
[ctf]: <https://ctftime.org/ctf-wtf/>
|
|
[cyberchallenge]: <https://cyberchallenge.it>
|
|
[ghc]: <https://gitlab.haskell.org/ghc/ghc>
|
|
[haskell-ita]: <https://haskell-ita.it>
|
|
[hs]: <https://haskell.org>
|
|
[nLab]: <https://ncatlab.org/nlab/show/HomePage>
|
|
[olicyber]: <https://olicyber.it>
|
|
[olimate]: <http://olimpiadi.dm.unibo.it>
|
|
[simplicial-sets]: <https://ncatlab.org/nlab/show/simplicial+set>
|
|
[the-hacker-crackdown]: <https://www.mit.edu/hacker/hacker.html>
|
|
[titos-catqm]: <https://github.com/jabberabbe/CatQM>
|
|
[toh]: <https://toh.necst.it>
|
|
[type-theory]: <https://plato.stanford.edu/entries/type-theory-intuitionistic/>
|
|
|
|
[comment]: # vim: ts=2:sts=2:sw=2:et:nojoinspaces:tw=80
|