Oh also, I'm quite interested in Linux and I like to configure my computer in my free time. But Operating Systems is such a broad subject that I don't really know where to start. Any suggestions would be welcomed!

I wouldn't consider myself retired from CP, and I'm not a CS major (I'm a math/econ major planning to pursue a Ph.D studying economic theory at the intersection of econ/CS theory), so I'm in no place to comment on any non-theoretical fields of CS. That said, in terms of interesting, CP-adjacent areas of CS, I'll put in a word for algorithmic game theory. Broadly, AGT as a field thinks about game theory problems from a CS perspective; this includes things like devising algorithms to compute equilibria of games or designing the rules of games such that the equilibrium achieves a certain desirable feature. One example of the latter scenario is called a knapsack auction: bidders each desire a certain amount of a good and derive some level of utility from receiving that much of the good, but you as the auctioneer can only give out a certain total amount of the good. If you knew each bidder's utility value, finding the welfare-maximizing allocation of the good to the bidders would be a standard knapsack problem. However, depending on the auction system you employ, bidders might bid strategically in order to receive their allocation at a lower cost; the resulting AGT problem involves designing this auction to incentivize bidders to bid truthfully and/or to maximize your own revenue.

Out of the fields of CS I've studied, AGT feels the most similar to CP in terms of the style of thinking involved. It's also relatively accessible (my class last semester used Twenty Lectures on Algorithmic Game Theory by Tim Roughgarden, which was relatively accessible, and I'm told that this book is a bit more advanced but is generally the standard reference), and the field is quickly expanding and still has lots of interesting research questions to explore.

Re: cold emailing professors--there's probably no harm in trying, but it may be hard to get a professor to dedicate time to working with you unless you give them a very compelling reason to take you on. As a result, if you do send cold emails, you should put substantial effort into them--for example, it will help if you can read some of the professors' papers and have insightful things to say about them.

Well, honestly I'm just starting CP but since this is about CS in general I'll offer my thoughts.

Personally I'm studying programming languages theory (and might I add, loving it).

PL Theory is exactly what it sounds like — the study of programming languages. This includes both the practical aspects (how to design a language) and also the more theoretical (the mathematical properties of PLs).

There is also a lot of intimate connections between CS and maths.

Consider the very beautiful notion of the Curry-Howard isomorphism : programs in a programming language correspond to proofs in a system of logic and types in the language correspond to propositions.

Curry-Howard is not "valid" for all programming languages in the sense that most statically typed mainstream languages (Java, C++, even the ones with more sensible type systems like Rust and Haskell) produce logical systems that are inconsistent — it is possible to prove false propositions. In fact, it can be shown that any Turing complete programming language must allow it's corresponding logic to prove false propositions.

We can exploit the Curry-Howard isomorphism to achieve some crazy feats.

Most of us think in type systems that only allow abstraction over types :

template <class T>
struct foo {
  // some data members or functions
};

Here foo is not a type but a type abstraction. It is only when we provide a concrete type for the parameter T that we get a valid type such as foo<int> or foo<vector<string>>.

This is great for a lot of applications but is not expressive enough for many things (or so we feel if we're studying PL theory).

There are languages, most notably the Calculus of Constructions and Martin-Lof's type theory (and their implementations Coq and Agda) that allow types that are abstract over terms.

Essentially, we can treat types as values themselves and manipulate them like regular objects.

Consider an example : let's try to define the set of all vectors (think finite lists) over a certain set. If we have an object of type vector<int> we know only one thing about it at compile-time : it is a vector of integers. There's no information about the number of elements it can potentially store.

We want our type of vectors to store this information in the type signature itself. So our type construction depends on two factors : the number of elements (a natural number) and the set over which we're constructing our type of vectors (such as strings, lists, etc.).

In order to define this, in say, Agda we would write the following recursive function :

Vec : Set -> Nat -> Set 
Vec A zero = Unit 
Vec A (succ n) = (Vec A n) * A

succ n simply means n + 1.

The type Vec A n now represents type of vectors over set A of length n. Let us try to understand the definition :

1. Vec A zero = Unit is the base case — there is only one vector of length so the set is the unit set (the set with only one meaningless element)
2. Vec A (succ n) = (Vec A n) * A is the inductive/recursive case — assuming we have already constructed Vec A n we simply take this type and do a cartesian product with the set A and define Vec A (succ n)

If you're wondering why we're using this weird succ n notation — there's a reason for that too.

The natural numbers are defined as an inductive datatype :

data Nat where 
  zero :: Nat 
  succ :: Nat -> Nat 

What this means is that there is some object zero and it is already known to be a Nat. The second line (the technical term is constructor) is an inductive definition — if n is known to be a Nat then succ n is also a Nat.

Mathematically, the natural numbers are anything that satisfies the Peano axioms. We can provide a mathematical model for inductive datatypes as defined in Agda and show that this definition of the natural numbers as an inductive datatype satisfies the Peano axioms (as far as I know).

We then define addition so that succ n happens to have the same meaning as adding by one. For more details — see the chapter on the natural numbers in PLFA.

The reason why dependent type programming is so powerful is that it is essentially equivalent to first-order logic (I'm skipping a few mathematical details) which is the formal language in almost of mathematics is written. By the Curry-Howard isomorphism, this means we can use langauges like Coq and Agda to verify mathematical proofs by converting them to computer programs in these langauges. This has actually been used to verify the proof of the four color theorem from graph theory. In fact, it was the world's first computer verified proof.

Agda code is not intuitive partly because it is such an expressive type system that everything can be treated both as a type and as a term of some type.

Look similar to my story I am tired of cp too and started to look at what I should do to get internship/job as a software engineer and found that I have missed studying topics like operating system, database and networking in advance.

I think after cp you realize that your life is not just on cp only (if your plan was to train intensively) and started to see how can you enjoy your life + for sure try to get an internship that will give you a good experience and let you see how things get done in the technical part

My advice is to try to re-prioritize things in your life and do what you think is the most important one. Best of luck in what you will choose to do :)