MVP_Harry's blog

By MVP_Harry, history, 10 days ago,

Hey there,

Two and a half years ago, I started doing CP, and it's a very fun and meaningful experience that I will cherish. But at some point, I just started growing tired of it (perhaps because I wasn't improving that much anymore), and I also realized that the computer science world is way larger than just CP.

So... what's after CP? What did you do after you "retired" from CP? Which area of CS did you explore?

I'm genuinely a bit lost and don't know what to do. For the past 6 months or so, I tried exploring stuff like Machine Learning, Computer Theory, and topics closer to theoretical CS, but felt like I wasn't making much progress without a teacher or a "partner" that could help me when I'm stuck (on that note, should I cold email university professors for research/learning opportunities?) I also don't know any stuff related to "developing" — I tried writing a chess engine in c++ and was also stuck, and I don't really know any of the programming languages that well.

For some context, I'm a high school rising senior living in the US. What should I do?

Thanks :)

• +104

 » 10 days ago, # |   +2 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!
•  » » 9 days ago, # ^ |   +1 You can start to read "operating system the three easy pieces" book by Remzi you will know a lot about how things going under the hood.
•  » » » 9 days ago, # ^ |   0 +1, am studying from it right now.
 » 10 days ago, # |   +96 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.
•  » » 10 days ago, # ^ | ← Rev. 2 →   +1 Thank you very much for the thoughtful response! AGT indeed sounds very interesting, and I will look into Twenty Lectures on Algorithmic Game Theory. Also, what do you think is the best way to self-study these rather advanced materials? Reading books? Perhaps a coursera course? What I really enjoyed about CP is that you have sites like cf and you can find get instant feedback of your progress (i.e. whether you solve the problem or not), but when I was reading some textbooks earlier, I couldn't get that feedback and couldn't feel the progress, which sometimes demotivate me.
•  » » » 10 days ago, # ^ |   +7 I've found reading books most helpful, but I generally learn much better from reading than from e.g. watching lectures. Coursera probably would offer more structure, so if textbooks haven't worked for you that might be more effective. OpenCourseWare might be another good source of lectures to work from.
 » 9 days ago, # | ← Rev. 4 →   +22 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 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 or foo>. 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 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 : 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) 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.